COMMENT ⊗   VALID 00014 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00003 00002	.if false then begin "what is needed"
C00006 00003	.s(PROVIN,PROVING FACTS ABOUT LISP PROGRAMS)
C00012 00004	.ss(formal,About Formalizing.)
C00018 00005	.ss(sexpth, The theory of S-expressions.)
C00036 00006	.ss(first, Summary of notion of formal theory.)
C00066 00007	.ss(lispth, |Lists, natural numbers and LISP program primitives.|)
C00075 00008	.ss(total,Representing programs known to terminate.)
C00106 00009	.ss(partial,Representing programs not known to terminate.)
C00125 00010	.ss(recpred,Recursively Defined Predicates.)
C00135 00011	.ss(induction, Additional induction principles for proving.)
C00150 00012	.ss(minim,Partial functions and the Minimization Schema.)
C00160 00013	.ss(lispax,Theory of LISP: Algebraic Axioms.)
C00167 00014	.next page
C00170 ENDMK
C⊗;
.if false then begin "what is needed"


	Unfortunately none of our examples use the general form
	of S-exp or  list induction  

Partial function 
	Would like an example of a naturally partial function that
could be reasonably easily proved partially correct using the minimization
schema.  

make comment that domain maps ⊗⊗f: ... qcross BOTTOM qcross ... → BOTTOM⊗ will
	not generally be explicitly mentioned.

appendix section summarizing theorems.

formulate a simple B/M recursion schema

formulate principle for domain construction with corresponding 
	recursion and induction principles

in recpred explain direct translation in case of termination
find syntactic criteria for termination

need example with λ in it

good short rank induction example

a third non trivial example, perhaps using min schema

need exercise for not known to term section

min schema for multiple recn

.end "what is needed"
.s(PROVIN,PROVING FACTS ABOUT LISP PROGRAMS)
.if NOTASSEMBLING then start
.PROVEX: NEXT SECTION!;
.IMPURE: NEXT SECTION!;
.MACHIN: NEXT SECTION!;
.SEARCH: NEXT SECTION!;
.EXTEND: NEXT SECTION!;
.ABSNTX: NEXT SECTION!;
.COMPIL: NEXT SECTION!;
.COMPUT: NEXT SECTION!;
.end

	In this chapter we begin the "Proving" part of the book.  
In particular we will explain a method for proving ⊗extensional 
properties of a restricted but powerful class of LISP programs which we call
⊗clean, ⊗pure LISP programs.  We will give a number of simple examples 
to illustrate the method.   The following chapter is devoted
to a few more complex examples.
We will see in later chapters how the proof techniques can be extended to
cover a larger class of properties and a larger class of programs.

	While the ultimate aim of proving programs is to replace debugging
by computer-checked proofs of program correctness, we aren't there yet.
However, even hand-checked proofs of correctness of small programs increase
our understanding of why programs work and improve the clarity and quality
of the programs we write.  If a suitable interactive proof-checker such as
Weyhrauch's FOL (xxxref) or Ketonen's EKL (xxxref) is available, a more
concrete understanding can be achieved.

	An ⊗extensional ⊗property is one that
depends only on the function computed by the program.
The fact that two sort programs compute the same function
and that ⊗append is associative are extensional facts, but
that one sort program does ⊗⊗n%52%*⊗ comparisons and another ⊗⊗n_log_n⊗
comparisons or that one program for ⊗reverse does fewer ⊗⊗cons⊗es than
another are not.  These latter facts are examples of ⊗intensional properties.
⊗Clean LISP programs have no side effects (our
methods require the freedom to replace a subexpression by any
expression that can be proved to have the same value),
and equality refers to the S-expressions and not to
the list structures in memory that represent them.
⊗Pure LISP involves only recursive function
definitions and doesn't use assignment statements.
So far we have only discussed how to write clean and pure LISP
programs.   The constructs to be explained in Chapter {SECTION IMPURE}
will take us out of this realm.

	The basic idea is to represent both programs and the properties 
we want to prove about them as sentences in first order logic.  
The methods of first-order logic are well developed and understood.  
Although we present the proofs somewhat informally, they can easily
be fully formalized.  After a brief introduction to the idea of 
formalization, we give an informal exposition of first order 
logic and describe the theories of S-expressions, lists and natural numbers.  
Next come techniques for proving properties of programs known in advance 
to always terminate.  After this 
come the more difficult techniques required when termination cannot be
assumed and termination or non-termination must be proved.


	We attempt to motivate and intuitively justify the methods of
representation of programs, but no formal proof of soundness
is given.   This is because our emphasis is on developing technique for
proving facts about specific programs rather than on developing a general
theory of program properties.  Thus our treatment is intended to be analogous
to that of a calculus text rather than that of a text in functions of a
real variable.
Much of the material in
this chapter is based on [[Cartwright and McCarthy 1979]].
An extensive treatment of other program proving techniques
is given in [[Manna 1974]].

.ss(formal,About Formalizing.)

	The main reason for developing formal methods is to be able to make
ideas and arguments clear and precise.  This wins in several ways.  
For the logicians the development of formal systems and methods of reasoning
allowed them to eliminate paradoxes which arose in informal arguments and 
also to prove many interesting things about their systems.
For the computer scientist formalization provides a way of making notions 
and reasoning precise enough to be checked and even generated by a computer.  
One goal is to make the computer do as much of the work as 
possible.

	In a formal system there are notions of syntax (properties of
the expressions of the language as strings of symbols), semantics (rules
determining meanings of expressions, i.e. what things the expressions stand
for), and
rules for manipulating syntactic entities in a semantics preserving manner.
Thus there are expressions formed from some given collection of symbols in
a prescribed manner, a means of assigning meaning to these expressions,
and often a notion of deduction.

	For example, a programming system is a formal system.  It has a
language consisting of the programs, usually specified by some sort
of grammar and recognized by a parser.

.if false then begin "change follows"
  The semantics of a program
can be specifed in terms of (partial) functions on some suitable abstract
domain (e.g. denotational semantics a la Scott and Strachey[]).
The rules are embodied an interpreter, compiler or some notion of computation.
For example a pure clean LISP programming system with semantics given as
(partial) functions on list structures and rules defined by 
⊗eval fits the paradigm nicely.
.end "change follows"

	For reasoning about programs we will use a formal system based on
first order logic.  
Understanding properties of a system based on first  order logic can be 
often be reduced to understanding properties of the underlying logic.  
This underlying logic is powerful and in general well understood.   
Such systems are determined by three basic components:
.begin nofill
.indent 5,5
.item ← 0

#. a domain with some designated subdomains (called sorts),
#. a language whose function and predicate symbols are interpreted in the domain and 
#. a collection of facts that are true of the domain.  
.end

	Given the basic  components, the expressions of the language, 
interpretation of these expressions
in the domain and rules for (syntactically) deducing additional facts
are fixed as we will explain below.

	Such a system can be mechanized in the following sense.  
We can write a program that is capable of accepting a description
of a logical system, build a data structure representing the various components,
check that statements are well-formed expressions of the language,
and that an alleged proof is indeed a valid deduction from the known facts.
Given such a program, we can describe to it our system for proving facts about
LISP programs and it will be able to check that our proofs are correct.  
Such program exists at Stanford [[Weyhrauch 1977]] and [[Ketonen and Weening 1981]].
Other programs exist which are designed to automatically prove facts about 
LISP programs.  For example see [[Boyer and Moore 1978]].  

.ss(sexpth, The theory of S-expressions.)

	We begin by simply presenting a formal theory, namely the
theory of S-expressions.  We present it as formalization  and abstraction
of the the discussion of S-expressions
given in Chapter {section READIN}.
The universe or domain in question contains S-expressions
and possibly other yet unspecified objects.  The goal is to
formalize properties of and syntactically characterize some 
sub-domains such as S-expressions, lists, and natural numbers 
(viewed as a subdomain of the atomic S-expressions).

	We first describe the language, some simple "boolean" facts
about the domain of S-expressions and give axioms describing
the algebraic properties of basic operations on S-expressions.
We then explain a principle of induction on S-expressions and
represent this principle by the schema of S-expression induction.
We deduce some additional properties of S-expressions as examples
of (semi-)formal proofs based on the formal description. 

Our precise notion of formal first order theory will be explained in the next 
section before we complete our description of the formal system for
reasoning about LISP programs.

.cb  |The elementary theory of ⊗car, ⊗cdr, and ⊗⊗cons⊗.|


	The domain of S-expressions we will denote by ⊗SEXP and the
subdomains consisting of the atoms and the non-atomic 
S-expressions we denote by ⊗ATOM and ⊗PAIR, respectively.  The fact
that S-expressions are the disjoint union of atoms and non-atoms
is expressed formally by the ⊗⊗domain relations⊗:
.begin nofill turnon "∂" group
.n←20

∂(n)⊗⊗SEXP = ATOM ∪ PAIR⊗
∂(n)⊗⊗ATOM ∩ PAIR = qEMPTY⊗
.end

	As in the external notation for LISP programs, we will
use list and/or dot notation for S-expression constants.  We mention
two particular atoms qT and qNIL.  Formally we specify that they are
of sort ⊗ATOM by the ⊗⊗domain membership facts⊗:
.begin nofill turnon"∂" group
.n←20

∂(n)⊗⊗qT ε ATOM⊗
∂(n)⊗⊗qNIL ε ATOM⊗
.end

	In order to make general statements about S-expressions 
we need variables.  We will use ⊗X, ⊗Y, ⊗Z as general variables.  
They stand for abitrary elements of the entire domain. 
There will also be variables for each of the sub-domains.  
⊗⊗x, y, z⊗ will stand for (range over) S-expressions, 
⊗⊗xx, yy, zz⊗ will stand for non-atomic S-expressions and 
⊗⊗a, b, c⊗ will stand for atoms.  
This is expressed formally by the additional domain membership facts:
.begin nofill turnon "∂" group
.n←20

∂(n)⊗⊗x, y, z ε SEXP⊗
∂(n)⊗⊗xx, yy, zz ε PAIR⊗
∂(n)⊗⊗a, b, c ε ATOM⊗
.end


	The basic functions on S-expressions are ⊗car, ⊗cdr and ⊗cons 
which we will denote by qqa, qqd and infix "_._" (or occasionally by qcons)
as in the external notation for programs.  That ⊗cons applied to any two 
S-expressions is a non-atomic S-expression and ⊗car and ⊗cdr applied to 
non-atomic S-expressions produce S-expressions is expressed formally by 
the ⊗⊗domain mappings⊗:
.begin nofill turnon "∂" group
.n←20

∂(n)⊗⊗qqa: PAIR → SEXP⊗
∂(n)⊗⊗qqd: PAIR → SEXP⊗
∂(n)⊗⊗qcons: SEXP qcross SEXP → PAIR⊗
.end

	We will treat ⊗SEXP, ⊗PAIR and ⊗ATOM as unary predicates on
the domain with the obvious meaning.

	Now some facts about ⊗car, ⊗cdr and ⊗cons.  
Recall that when an S-expression is constructed from
two given S-expressions, the result has the first S-expression in
the a-part and the second in the d-part.  This is stated formally
by the axioms:

.begin nofill turnon "∂"
.n←20

∂(n)$$CAR:$__⊗⊗∀x y.qa [x_._y] = x⊗
∂(n)$$CDR:$__⊗⊗∀x y.qd [x_._y] = y⊗
.end

Since ⊗x, and ⊗y are specified to range over S-expression, the
quantifier ⊗⊗∀x y.⊗ means "for all S-expressions ⊗x and 
for all S-expressions ⊗⊗y⊗".  

	Also given a non-atomic S-expression ⊗xx, the S-expression
constructed from ⊗⊗qa xx⊗ and ⊗⊗qd xx⊗ is qequal to ⊗xx 
Thus

.begin nofill turnon "∂"
.n←20

∂(n)$$CONS:$__⊗⊗∀xx.[qa xx_._qd xx] = xx⊗
.end

Since ⊗xx is specified to range over non-atomic S-expressions, the
quantifier ⊗⊗∀xx.⊗ means "for all non-atomic S-expressions ⊗⊗xx⊗" or
"for all pairs ⊗⊗xx⊗".  
The axiom $CONS also expresses the fact that two S-expressions are
equal if and only if their a-parts are equal and their d-parts are equal.
That is:
.begin nofill turnon "∂"
.n←20

∂(n)$$EQPAIR:$__⊗⊗∀xx yy.[[qa xx = qa yy] ∧ [qd xx = qd yy] ≡ xx = yy]⊗
.end

	We can even give a formal proof that $EQPAIR is true in the
theory developed so far.   
To prove that a statement holds for all ⊗⊗xx, yy⊗ it is enough to prove
that the unquantified statement holds without making any special assumptions
about ⊗xx or ⊗yy.  Thus we want to prove

⊗⊗⊗[qa xx = qa yy] ∧ [qd xx = qd yy] ≡ xx = yy⊗

To prove that a formula of the form ⊗⊗A ≡ B⊗ is true it is sufficient to
prove that ⊗⊗A ⊃  B⊗ and ⊗⊗B ⊃ A⊗ are both true since equivalence is 
really  an abbreviation of the conjunction of the two implications.
So we must prove

.begin nofill

⊗⊗⊗[qa xx = qa yy] ∧ [qd xx = qd yy] ⊃ xx = yy⊗
and
⊗⊗⊗xx = yy ⊃ [qa xx = qa yy] ∧ [qd xx = qd yy] ⊗
.end

To prove ⊗⊗A ⊃ B⊗ we assume ⊗A and show that ⊗B follows.
For the first implication, assume 

⊗⊗⊗[qa xx = qa yy] ∧ [qd xx = qd yy].⊗

Then by substitition of equals for equals we have

⊗⊗⊗[qa xx . qd xx] = [qa yy . qd yy]⊗

and using $CONS twice we obtain the desired conclusion

⊗⊗⊗xx=yy.⊗

For the second implication, assume 

⊗⊗⊗xx=yy.⊗  

Then

⊗⊗⊗[qa xx = qa yy] ∧ [qd xx = qd yy]⊗

follows by subsititution.  This completes the proof.

	The above proof was carried out in a 
"natural deduction" style and could be completely formalized
(for example so as to be accepted by a proof checker for
natural deduction style proofs)  without much additional detail.

[Remark:
A first order theory deduced by formal proof from given 
axioms will hold in any domain where the given axioms hold.  Thus
we are really proving things about a class of domains, not just
one.
]

.cb The principle of S-expression induction.

	With the axioms and domain facts given so far we can use
the rules of logic to prove many addiditonal facts about particular
S-expressions and a few general facts, but there are many facts
about S-expressions that can not be proved.  For example in the domain
of S-expressions we have

$NO-RPLACS: ___⊗⊗∀x y: x≠[x_._y]⊗

but this is not provable in the theory developed so far.  
Indeed there are domains where the facts given so far are true, 
but ⊗⊗∃x_y:_x=[x_._y]⊗ is also true.
(The significance of the label $NO-RPLACS will become clear in
Chapter {section IMPURE} where we discuss operations that create circular list
structures.)
That says that the algebraic and domain facts are insufficient
to characterize S-expressions.
Indeed Goedel's famous theorem extends to tell us that no
theory in which all proofs can be checked admits proofs of all true
statements about S-expressions.  However, all practically interesting
sentences involving pure LISP programs are provable in the above
theory supplemented by a suitable principle of mathematical induction.

.if false then begin "change follows"
  Although it is impossible to completely
characterize, in a reasonable syntactic way,  a domain as rich as
the domain of S-expressions we can certainly do better.
(A complete characterization could be given by listing all true facts,
but this is not considered resonable and it can not be done "effectively".)
.end "change follows"


	Recall the "inductive" definition of S-expression:
an S-expression is either an atom or 
it is the result of applying ⊗cons to the ⊗car and the ⊗cdr.  
Further more each S-expression is the result of a finite number of
⊗⊗cons⊗es begining with a finite number of atoms.  
Thus if some property is true of all atoms and 
whenever it is true of ⊗x and ⊗y it is true of ⊗⊗[x_._y]⊗ then 
it will be true of all S-expressions.
This is expressed formally by the S-expression induction schema:

$SEXPINDUCTION: ⊗⊗⊗∀a: qP a ∧ ∀xx: [qP qa xx ∧ qP qd xx ⊃ qP xx] ⊃ ∀x: qP x ⊗.

Here qP is a predicate parameter.  The schema is used by subsituting a unary
predicate expression (a formula with a designated variable which is to be
replaced by the argument to qP) for qP.  Thus the schema stands for
an infinite collection of axioms, one for each formula and designated
(free) variable that formula.

	Using S-expression induction we can prove $NO-RPLACS: ___⊗⊗∀x y: x≠[x_._y].⊗
Instantiating $SEXPINDUCTION with ⊗⊗qP_x_≡∀y:_x≠[x_._y]⊗ we obtain the
particular axiom

⊗⊗⊗∀a y: a ≠[a_._y] ∧ ∀xx: [∀y: qa xx≠[qa xx_._y]∧∀y: qd xx≠[qd xx_._y] ⊃ ∀y: xx≠[xx_._y]] ⊃ ∀x y: x≠[x_._y].⊗

Thus to prove ⊗⊗∀x y:x≠[x_._y]⊗  it is sufficient to prove the two clauses in
the hypothesis.  The clause for the ATOM case is ⊗⊗∀a_y:_a ≠[a_._y].⊗ 
We prove it by contradiction.   That is we assume the negation, ⊗⊗a=[a_._y]⊗,
holds for some atom ⊗a and S-expression ⊗y.  Then we have by the domain relations,
function mappings and the fact that ⊗a ranges over atoms the following:

⊗⊗⊗ATOM a ∧ PAIR [a_._y] ∧ ATOM ∩ PAIR = qEMPTY.⊗

Clearly a contradiction.

The clause for the non-ATOM case is

⊗⊗⊗∀xx: [∀y: qa xx≠[qa xx_._y]∧∀y: qd xx≠[qd xx_._y] ⊃ ∀y: xx≠[xx_._y]].⊗  

It is proved by assuming ⊗⊗∀y: qa xx≠[qa xx_._y] ∧ ∀y: qd xx≠[qd xx_._y] ⊗ 
(the induction hypothesis) an deducing ⊗⊗∀y:_xx≠[xx_._y]⊗.  
The latter is again done by contradiction.  Assume for some S-expression ⊗y 
that ⊗⊗xx=[xx_._y]⊗.
Then by substitution and $CAR we have ⊗⊗qa xx=qa [xx_._y]=xx⊗.  
Substituting again we get ⊗⊗qa xx=[qa xx_._y]⊗ which contradicts the 
induction hypothesis, completing the proof.

	S-expression induction is on example of a class of induction
principles known as "structural" induction.   Such principles are
based directly on the inductive definition of the domain to which
they apply.  We will later add principles of list and numcerical
induction which are also structural induction principles.

	S-expression induction could be introduced as a proof rule
rather than an axiom schema.
To prove that some formula ⊗⊗qP_x⊗ holds for all S-expressions, 
⊗x  (i.e. to prove ⊗⊗∀x:_qP_x⊗)  it is sufficient to 
.begin nofill group

    (i) prove the ATOM case: ⊗⊗∀a: qP a⊗
and
    (ii) assume the induction hypotheses: ⊗⊗qP qa xx⊗ and ⊗⊗qP qd xx⊗ and prove from them ⊗⊗qP xx⊗.
.end

This is essentially what we did in carrying out the above proof.  

	Notice that we have so far not mentioned any defined functions.
The theory won't be of great practical value until we tell how to do it,
but in exchange for restraint we get a bonus.  Derek Oppen [[1978]] has
given an algorithm for deciding whether any sentence of the theory so
far is true.  He has shown that any such algorithm must be very slow
in general, but there is reason to hope that in practical cases, the
algorithm will be fast enough.
.ss(first, Summary of notion of formal theory.)

	Now we will make precise our notion of first order theory
of which the theory of S-expressions is an example.  
As mentioned before, the basic components of such a theory are 
a domain with some designated subdomains (called sorts) 
a language whose predicate and function symbols are interpreted in the domain and 
a collection of facts that are true of the domain.  
What we need to do is make clear the process used to describe the
basic components and to show how this description determines
the well-formed expressions of the language, 
their interpretation in the domain of interest and 
say what the rules for (syntactically) deducing additional facts.

	We assume that the domain of interest, its subdomains, and
a collection of functions and predicates on the domain are known
(given by some independent means).   Our description of a theory
will have the following basic outline:
.begin nofill

(i) List the sort symbols and specify the subdomain denoted by each.

(ii) Present the domain relations.  (See the discussion of %3facts%*.)

(iii) List the constants for each sort, and specify the object denoted by each one.

(iv) List the variable ranging over each sort.

(v) List the function symbols, specifying the function denoted.

(vi) Give domain maps for each function symbol.

(vii) List the predicate symbols, giving the predicate denoted by each.
______Sort symbols are considered to be unary predicate symbols with the obvious denotation.
______"=" is assumed to be a binary predicate symbol with the standard interpretation

(viii) Give the axioms.
.end

The non-logical symbols are then the sort symbols, the constant and variable
symbols, the function symbols and the additional predicate symbols.
If qx is a variable of sort ⊗D then we will also use qxq0, qxq1, ... as
variables of that sort.
Note that each function and predicate symbol has a fixed number of arguments 
called the arity.  (This is determined when the function or predicate
denoted by the symbol is specified.)

	The above form of description defines the basic theory.  This
theory will be extended from time to time by adding additional function
and predicate symbols and defining axioms.

.cb The Language.

	Now we describe how the expressions of the language are built 
once the non-logical symbols have been given.  There are four classes
of expressions:  terms, formulas, function expressions, and predicate
expressions.  Terms denote objects (individuals) in the domain, 
formulas denote truthvalues, function and predicate expressions denote 
functions and predicates on the domain.  We define the four classes
of expressions inductively.  Terms are used in making formulas, 
and formulas occur in terms so that the definitions are ⊗mutually ⊗recursive.  
Function and predicate expressions are also involved in the mutual recursion.

%3Terms%1: Constants are terms, and variables are terms.  If
qq is a function expression taking ⊗n arguments, and ⊗⊗tq1,_..._,tq-⊗
are terms, then ⊗⊗qq[tq1,_..._,tq-]⊗ is a term.  If ⊗A is
a formula and ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms, then
[⊗⊗IF_A_THEN_tq1_ELSE_tq2⊗] is a term.  
Some examples of terms in the theory of S-expressions are:
.begin nofill turnon "∂" group
.n←24

∂(n)   (i)   qNIL
∂(n)  (ii)   ⊗⊗x⊗
∂(n) (iii)   ⊗⊗qa x⊗
∂(n)  (iv)   ⊗⊗IF ATOM x THEN x ELSE qd x⊗
.end

%3Function expressions%1: A function symbol is a function expression.
If ⊗⊗qxq1,_..._,qxq-⊗ are general variables and ⊗t is a term, then
⊗⊗[λqxq1,_..._,qxq-:_t]⊗ is a function expression.

%3Predicate expressions%1: A predicate symbol is a predicate expression.
If ⊗⊗qxq1,_..._,qxq-⊗ are general variables and ⊗A is a formula, then
⊗⊗[λqxq1,_..._,qxq-:_A]⊗ is a predicate expression.

.xgenlines←xgenlines-2

Some examples of function and predicate expressions are:
.begin nofill turnon "∂" group
.n←24

∂(n)   (v)   qqa 
∂(n)  (vi)   ⊗⊗SEXP⊗
∂(n) (vii)   ⊗⊗λX: IF ATOM X THEN X ELSE qd X⊗
.end

%3Formulas%1:
If qp is a predicate expression taking ⊗n arguments and
⊗⊗tq1,_..._,tq-⊗ are terms, then ⊗⊗qp[tq1,_..._,tq-]⊗ is a formula.
In particular, if ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms then ⊗⊗tq1_=_tq2⊗ is a formula.
If ⊗A, ⊗B, ⊗C are formulas, then ⊗⊗¬A⊗, ⊗⊗A_∧_B⊗, ⊗⊗A_∨_B⊗, ⊗⊗A_⊃_B⊗, ⊗⊗A_≡_B⊗,
and ⊗⊗IF_A_THEN_B_ELSE_C⊗ are formulas.  
If ⊗⊗qxq1,_...,_qxq-⊗ are variables, and ⊗A is a formula, then
⊗⊗[∃qxq1_..._qxq-:_A]⊗ and ⊗⊗[∀qxq1_..._qxq-:_A]⊗ are formulas.
Some examples of formulas in the theory of S-expressions are:
.begin nofill turnon "∂" group
.n←24

∂(n)(viii)   ⊗⊗qa x = qd x⊗
∂(n)  (ix)   ⊗⊗ATOM X⊗
∂(n)   (x)   ⊗⊗IF ¬ATOM x THEN qa x = qd x ELSE qT = qT⊗
∂(n)  (xi)   ⊗⊗∀x: [PAIR x ⊃ ∃y z: x = y . z]⊗

.end

	An occurrence of a variable qx is classified as ⊗bound or
⊗free according to the following rule.  qx is bound in
an expression of one of the forms ⊗⊗[λqxq1_..._qxq-:_t]⊗,
⊗⊗[λqxq1_..._qxq-:_A]⊗, ⊗⊗[∀qxq1_..._qxq-:_A]⊗ or ⊗⊗[∃qxq1_..._qxq-:_A]⊗
if it is one of the numbered qx's.  
An occurrence of qx in an expression ⊗e is bound if that occurence is
bound in some subexpression of ⊗e.  Otherwise it is free.
A formula having no free variables is called a ⊗sentence.  
Thus ⊗X is bound in example (vii)  but not in (ix).
The formula of example (xi) is a sentence.

	We note that conditional expressions and λ-expressions are 
not ordinarily included in a first order language.  These extensions 
do not change the logical strength of the theory, because, as we shall see, every
formula that includes conditional expressions or λ-expressions can be
transformed into an equivalent formula without them.  However, the
extensions are practically important, because they permit us to use
recursive definitions directly as formulas of the logic.  

.cb Assigning meaning to expressions.

	Next we explain how to determine the meaning of an expression
in the domain of interest (or any domain where the non-logical symbols
have been assigned an appropriate meaning).__ 
The meaning of expressions containing free variables can not be determined,
in general, without assigning a value to each of the variables.  
We say that an assignment is "allowed" if the variable is general or if it 
ranges over a subdomain ⊗D and the value assigned is in that subdomain.
So, we will imagine a fixed but arbitrary interpretation assigning allowed
values to each variable of the language.  Meanings are then relative to
such an interpretation.  Meanings are determined inductively in a manner
parallel to the construction of expressions.

%3Terms%1: The meaning of a constant is the object that it denotes.  The 
meaning of a variable is the value assigned to it by  the interpretation.
If qq is a function expression taking ⊗n arguments, and ⊗⊗tq1,_..._,tq-⊗
are terms, then the meaning of ⊗⊗qq[tq1,_..._,tq-]⊗ is the value 
of the function assigned to qq when applied to the values assigned to
the terms ⊗⊗t%4i%*.  If ⊗A is a formula and ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms, 
if ⊗A is true then the value assigned to ⊗⊗IF_A_THEN_tq1_ELSE_tq2⊗ is 
the value assigned to ⊗⊗tq1⊗, otherwise it is assigned the value
assigned to ⊗⊗tq2⊗.

In the theory of S-expressions, if the value assigned to ⊗x is $$(A . B)$
then the meanings of the terms given in examples (i)-(iv) above are:
.begin nofill turnon "∂" group
.n←24

∂(n)   (i)   qNIL
∂(n)  (ii)   $$(A . B)$
∂(n) (iii)   $A 
∂(n)  (iv)   $B 
.end

%3Function and predicate expressions%1: Function and predicate symbols
are assigned the function or predicate denoted by the symbol.
The expression ⊗⊗[λqxq1,_..._,qxq-:_e]⊗ is assigned a function or
predicate according to whether ⊗e is a term or formula.  The value
of ⊗⊗[λqxq1,_..._,qxq-:_e][tq1,_..._,tq-]⊗  the value assigned to
⊗e relative to an interpretation which is modified by assigning the
values of the ⊗⊗t⊗s to the corresponding qxs.

This is our reason for only allowing λ-binding
of general variables.  Namely if we allowed binding of sorted variables
then some terms would not have well defined values, and this is not
in the spirit of first order logic.   Another approach would be
to allow λ-binding of any variable, but only allow application of
such expressions to terms of the appropriate sort.  This makes
the class of well-formed expressions undecidable which is undesirable
if we wish to represent our system is in a computer.

.xgenlines←xgenlines-2

%3Formulas%1:
If qp is a predicate expression taking ⊗n arguments and
⊗⊗tq1,_..._,tq-⊗ are terms, then ⊗⊗qp[tq1,_..._,tq-]⊗ is true 
exactly when the tuple of values assigned to the ⊗⊗t⊗s satisfies
the predicate assigned to qp.
In particular, if ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are terms then ⊗⊗tq1_=_tq2⊗ is true 
exactly when ⊗⊗tq1⊗ and ⊗⊗tq2⊗ are assigned the same value.
If ⊗A, ⊗B, ⊗C are formulas, then ⊗⊗¬A⊗, is true exactly when ⊗A is false,
⊗⊗IF_A_THEN_B_ELSE_C⊗ is true if ⊗A is true and ⊗B is true or if ⊗A is
false and ⊗C is true and false otherwise.  The values of 
⊗⊗A_∧_B⊗, ⊗⊗A_∨_B⊗, ⊗⊗A_⊃_B⊗, and ⊗⊗A_≡_B⊗ are determined from the
values assigned to ⊗A and ⊗B according to the following truthtable:
.xgenlines←xgenlines-2
.begin nofill turnon "∂" 
.group
.n1←20;n2←28;n3←36;n4←44;n5←52;n6←60;

∂(n1+1)⊗⊗A⊗∂(n2+1)⊗⊗B⊗∂(n3+1)∧∂(n4+1)∨∂(n5+1)⊃∂(n6+1)≡

∂(n1)qtrue∂(n2)qtrue ∂(n3)qtrue∂(n4)qtrue∂(n5)qtrue∂(n6)qtrue
∂(n1)qtrue∂(n2)qfalse∂(n3)qfalse∂(n4)qtrue∂(n5)qfalse∂(n6)qfalse
∂(n1)qfalse∂(n2)qtrue∂(n3)qfalse∂(n4)qtrue∂(n5)qtrue∂(n6)qfalse
∂(n1)qfalse∂(n2)qfalse∂(n3)qfalse∂(n4)qfalse∂(n5)qtrue∂(n6)qtrue

!tabletruth The semantics of logical connectives.!
.end


If ⊗⊗qxq1,_...,_qxq-⊗ are variables, and ⊗A is a formula, then
⊗⊗[∀qxq1_..._qxq-:_A]⊗ is true exactly if ⊗A is true for all allowed
interpretations of the variables differing from the fixed one only in
assignments made to the variables qx%4i%*.
⊗⊗[∃qxq1_..._qxq-:_A]⊗ is true exactly if there is some allowed
interpretation of the variables differing from the fixed one only in
assignments made to the variables qx%4i%*.

In the theory of S-expressions, if the value assigned to ⊗x is $$(A . B)$
then the meanings of the formulas given in examples (viii)-(x) above are:
.begin nofill turnon "∂" group
.n←24

∂(n)(viii)   qfalse
∂(n)  (ix)   qfalse
∂(n)   (x)   qfalse
.end

while if the value assigned to ⊗x is $$(A . A)$
then the meanings of the formulas given in examples (viii)-(x) above are:
.begin nofill turnon "∂" group
.n←24

∂(n)(viii)   qtrue
∂(n)  (ix)   qfalse
∂(n)   (x)   qtrue
.end

The formula of example (xi) is true for any interpretation of the variables.
Since it is a sentence, its truth or falsity doesn't depend on the values
assigned to the variables.

	Those who are familiar with the lambda calculus should note
that λ is being used here in a very limited way.  Namely, the variables
in a lambda-expression take only elements of the domain as values,
whereas the essence of the lambda calculus is that they take arbitrary
functions as values.  We may call these restricted lambda expressions
⊗⊗first-order lambdas⊗.  


.cb Facts

	Facts come in two flavors: domain facts and axioms.  Axioms
are simply sentences of the language that we are asserting to be 
true in the domain.  There are three way of expression domain facts:
as domain relations, as domain membership specifications and as
domain mappings for functions.  The use of domain expressions
is a matter using a more natural notation.  As we will see each
expression of a domain fact has an equivalent axiom.

	Domain terms are formed from sort symbols and finite subdomain
descriptions of the form α{qzq1,_..._,qzq-} using the
binary boolean operations ∪ and ∩ meaning union and intersection.
Domain relations are formed from domain terms using the binary
relations symbols = and ⊂ meaning equality and containment.
The axioms corresponding to the domain relations for the theory
of S-expressions are:
.begin nofill turnon "∂" group
.l←10 m←35 n←45

∂(l)⊗⊗SEXP = ATOM ∪ PAIR⊗  ∂(m)↔ ∂(n)⊗⊗∀X: [SEXP X ≡ ATOM X ∨ PAIR X]⊗
∂(l)⊗⊗ATOM ∩ PAIR = qEMPTY⊗  ∂(m)↔ ∂(n)⊗⊗∀X: ¬[ATOM X ∧ PAIR X]⊗
.end

Domain membership facts have the form:

⊗⊗⊗qz ε D %1or%* qx ε D⊗

where qz denotes a constant symbol, qx denotes a variable symbol and
⊗D denotes a sort symbol.  The corresponding axioms are:

⊗⊗⊗D qz %1or%* ∀qx: D qx.⊗

Function mappings have the general form:

⊗⊗⊗F: Dq1 qcross_..._qcross Dq- → Dq0⊗

which corresponds to  the axiom:

⊗⊗⊗∀Xq1_..._Xq-: [Dq1 Xq1 ∧_..._∧ Dq- Xq-] ⊃ Dq0 F[Xq1_..._Xq-]]⊗

where the D%4i%* denote sort symbols and F denotes a function symbol 
taking ⊗n arguments.

.cb Rules

	There are many possible formal proof systems (collections of rules 
for deducing facts).  The natural deduction system mentioned in
qsect {subsection sexpth} is one possibility.   Basically any rule
that only allows deduction from given facts of facts that are true in any 
domain where all of the given facts are true is a valid rule.  
We will not specify any particular proof rules.  
However, the proofs presented will be, for the most part, informal versions
of "natural" deduction proofs augmented by extended substitution rules
and tautologies.   In fact most of the proofs have been carried out formally
in such a system and confirmed by a proof-checker.
Since the use of sorted variables, conditional expressions and first order
lambdas are not standard, we give some rules below for treating them.

.bb Manipulating quantifiers over sorted variables.

.if false then begin "change follows"
.end "change follows"

	In order to shorten formulas, we use sorted variables.  Thus
we can write ⊗⊗∀xx:[qa xx_._qd xx_=_xx)⊗, taking advantage of the fact
that the variable ⊗xx ranges only over non-atomic S-expressions,
instead of having to write ⊗⊗∀x.[¬ATOM_x_⊃_qa x_._qd x_=_x]⊗.
The proofs are also shortened, since we can avoid having to
prove ⊗⊗¬ATOM_xx⊗ every time the fact is needed.

	The usual rules given for manipulating quantifiers 
(generalization, specializtion, etc.)
apply to variables that range over the entire domain.  In order
to handle variables restricted to range over some subset we must either
modify the rules or show how to eliminate the restricted variables from
a formula.  Since we have given no rules to modify, we will indicate
how quantifiers over sorted variables can be eliminated.  Given
a particular set of rules, it would be better to extend them to
handle sorted variables using the elimination rules as a guide.
Otherwise the purpose of introducing them is defeated.

	Suppose the variable qx is restricted to range over the subdomain
⊗D and the variable qxq1 is a general variable.  
For example, in the theory of S-expressions we have the subdomain
⊗SEXP, with the variable ⊗⊗x_ε_SEXP⊗ and ⊗X is a general variable.
The formula ⊗⊗∀qx:A⊗ is then equivalent to ⊗⊗∀qxq1:[D_qxq1_⊃_A]⊗ and
the formual ⊗⊗∃qx:A⊗ is equivalent to ⊗⊗∃qxq1.[D qxq1 ∧ A]⊗.

.bb Rules for Conditional Expressions.

	All the properties we shall use of conditional terms follow
from the relation

!eqncond1 ⊗⊗⊗[A ⊃ [IF A THEN tq1 ELSE tq2] = tq1] ∧ [¬A ⊃ [IF A THEN tq1 ELSE tq2] = tq2] ⊗.

	It is worthwhile to list separately some properties
of conditional terms.  First we have the obvious
.begin nofill group

⊗⊗⊗[IF qtrue THEN tq1 ELSE tq2] = tq1		⊗
!eqncond2 
⊗⊗⊗[IF qfalse THEN tq1 ELSE tq2] = tq2.		⊗
.end

Next we have a ⊗distributive ⊗law for functions applied
to conditional terms, namely

!eqncond4 ⊗⊗⊗f[IF A THEN tq1 ELSE tq2] = IF A THEN f[tq1] ELSE f[tq2] ⊗.

This applies to predicates as well as functions and can also be used
when one of the arguments of a function of several arguments is a
conditional term.  It also applies when one of the terms of
a conditional term is itself a conditional term.

Thus
.begin nofill group

!eqncond5 ⊗⊗⊗IF [IF A THEN B ELSE C] THEN tq1 ELSE tq2 =					⊗
⊗⊗⊗IF A THEN [IF B THEN tq1 ELSE tq2] ELSE [IF C THEN tq1 ELSE tq2]⊗
and
⊗⊗⊗IF A THEN [IF B THEN tq1 ELSE tq2] ELSE tq3 =						⊗
!eqncond6 ⊗⊗⊗IF B THEN [IF A THEN tq1 ELSE tq3] ELSE [IF A THEN tq2 ELSE tq3] .		⊗
.end
	When the expressions following THEN and ELSE are
formulas, then the conditional expression can be replaced by a formula
according to

!eqncond7 ⊗⊗⊗[IF A THEN B ELSE C] ≡ [A ∧ B] ∨ [¬A ∧ C] ⊗.

These rules permit eliminating conditional expressions from formulas
by first using distributivity to move the conditionals
to the outside of any functions or predicates and then replacing the conditional
expression by a Boolean expression.   They could be added to our formal proof
system either as rules or as axiom schemata.

	More facts about conditional terms are given in [McCarthy 1963]
including a discussion of canonical forms that parallels the canonical
forms of boolean terms.  Any question of equivalence of conditional
terms is decidable by truth tables analogously to the decidability of
propositional sentences.

.bb Lambda-expressions.

	The only rule required for handling lambda-expressions
in first order logic is called ⊗lambda-conversion.  Essentially it is

⊗⊗⊗[λqx: e][t] =⊗ < the result of substituting ⊗t for qx in ⊗e >.

As examples of this rule, we have

⊗⊗⊗[λx: qa x . y][u . v] = [qa [u . v]] . y .		⊗

However, a complication requires modifying the rule.  Namely,
we can't substitute for a variable qx an expression ⊗e that has a free variable
qxq1 into a context in which qxq1 is bound.  Thus it would be
wrong to substitute ⊗⊗qxq1+_qxq2⊗ for qx in ⊗⊗∀qxq1:_[qx_+_qxq1_=_qxq2]⊗ or into
the term ⊗⊗[λqxq1:_qx_+_qxq1][u_+_v]⊗.  Before doing the substitution, the
variable qxq1 would have to be replaced in all its bound occurrences by
a new variable.  

	Lambda-expressions can always be eliminated from sentences and
terms by lambda-conversion, but the expression may increase greatly
in length if a lengthy term replaces a variable that occurs more than
once in ⊗e.  It is easy to make an expression of length proportional to ⊗n whose
length is proportional to 2%5n%* 
after conversion of its ⊗n nested lambda-expressions.
For example 
	
⊗⊗⊗λqxq1: [qxq1.qxq1][ ... [λqxq-: [qxq-.qxq-][$$A$]] ... ]⊗

becomes 

		$$(A . A)$,

		$$((A . A) . (A . A))$,

or
.begin nofill 

		$$((((A . A) . (A . A)) . ((A . A) . (A . A))) $
		$$  . ((A . A) . (A . A)) . ((A . A) . (A . A))))$
.end
for ⊗n = 1, 2, or 4 respectively.

	The use of λ-expressions in writing programs also may improve
efficiency by specifying some the expression be evaluated once and
the value used in several places.  Where there are side-effects, of
course more than efficiency is affected.
.ss(lispth, |Lists, natural numbers and LISP program primitives.|)

	We now extend the theory of S-expressions in order to talk about
the subdomain of lists and natural numbers.   We also define functions
corresponding to the basic LISP programs other that ⊗car, ⊗cdr and ⊗cons that
were described in Chapter {section READIN}.

.bb The Theory of lists.

	The domain of lists is a subdomain of the domain of S-expressions
which we denote by ⊗LIST.  It is the union of the one element 
domain ⊗NULL and the domain of non-empty lists ⊗NELIST.  These domain facts
are given by

.begin nofill turnon "∂" turnoff "{}"
.n←20

∂(n)⊗⊗LIST ⊂ SEXP⊗
∂(n)⊗⊗NELIST ⊂ PAIR⊗
∂(n)⊗⊗NULL = {qNIL}⊗
∂(n)⊗⊗LIST = NULL ∪ LIST⊗
∂(n)⊗⊗NULL ∩ NELIST = qEMPTY⊗
.end

The variables ⊗⊗u, v, w⊗ will range over lists and
⊗⊗uu, vv, ww⊗ will range over non-empty lists.

.begin nofill turnon "∂"
.n←20

∂(n)⊗⊗u, v, w ε LIST⊗
∂(n)⊗⊗uu, vv, ww ε NELIST⊗
.end

	The behaviour of ⊗car, ⊗cdr and ⊗cons on the domain ⊗LIST 
is given by the function mappings:

.begin nofill turnon "∂"
.n←20

∂(n)⊗⊗qqa: NELIST → SEXP⊗
∂(n)⊗⊗qqd: NELIST → LIST⊗
∂(n)⊗⊗qcons: SEXP qcross LIST → NELIST⊗
.end

	Since lists are a subdomain of S-expressions and non-empty lists
a subdomain of non-atomic S-expressions the axioms $CAR, $CDR and $CONS 
apply to lists also.  For lists we have the following structural induction
principle.

$LISTINDUCTION: ⊗⊗⊗qP qNIL ∧ ∀uu: [qP qd uu ⊃ qP uu] ⊃ ∀u: qP u ⊗.

.bb Natural numbers.

	We will treat the domain of natural numbers as a subdomain of
the atoms.  This reflects the way LISP systems treat numbers and makes
it possible to discuss mixed symbolic and numeric expressions conveniently.
The natural numbers will be denoted by ⊗NATNUM and is the union 
of the one element domain ⊗ZERO and the domain of positive numbers ⊗POSP.  

.begin nofill turnon "∂" turnoff "{}"
.n←20

∂(n)⊗⊗NATNUM ⊂ ATOM⊗
∂(n)⊗⊗ZERO = {$$0$}⊗
∂(n)⊗⊗NATNUM = ZER0 ∪ POSP⊗
∂(n)⊗⊗ZERO ∩ POSP = qEMPTY⊗
.end

	We will use the ordinary numerals $0, $1, $2, etc. to 
denote numbers. 
The variables ⊗⊗l, n, m⊗ will range over numbers and
⊗⊗ll, mm, nn⊗ will range over positive numbers.

.begin nofill turnon "∂"
.n←20

∂(n)⊗⊗l, n, m ε NATNUM⊗
∂(n)⊗⊗ll, mm, nn ε POSP⊗
.end

	The basic functions on numbers are ⊗successor and ⊗predecessor 
which we will denote by ⊗add1 and ⊗sub1 corresponding to names of the
LISP programs that compute these functions.  ⊗add1 maps numbers to wo 
positive numbers and ⊗sub1 maps positive numbers to numbers.

.begin nofill turnon "∂"
.n←20

∂(n)⊗⊗add1: NATNUM → POSP⊗
∂(n)⊗⊗sub1: POSP → NATNUM⊗
.end

.begin nofill turnon "∂"
.n←20

∂(n)$$SUB1:$__⊗⊗∀n: sub1 add1 n = n⊗
∂(n)$$ADD1:$__⊗⊗∀nn: add1 sub1 nn = nn⊗
.end

.if false then begin "change follows"
NOT QUITE THE USUAL FORM
.end "change follows"
Our form of the induction principle for natural numbers is:

$NUMINDUCTION: ⊗⊗⊗qP $0 ∧ ∀nn: [qP sub1 nn ⊃ qP nn] ⊃ ∀n: qP n.⊗

	This ends the description of the basic theory of S-expressions,
lists and numbers.   Our theory is a dynamic one, however, and we 
will introduce new function and predicate symbols with defining
axioms as we proceed.  

[Remark:  there are domains other than S-expressions where the facts
we have specified hold.  For example we have not specified the 
value of ⊗car and ⊗cdr on atoms, and there are many consistent
possiblilities.  The additional facts we can prove using any 
valid proof rules will also be true in a such domain.]


.bb Axioms for basic LISP programs.

	As advertised, we are going to extend the basic theory by
defining new functions and predicates.
In order to represent LISP programs as functions in a first
order theory, we first need to represent the basic programs.  We have
already introduced ⊗car, ⊗cdr and ⊗cons.  For the rest we add
the ternary function symbol qif, to represent the conditional.  We
will generally write 

⊗⊗⊗qif tq0 qthen tq1 qelse tq2 %1 instead of %* qif[tq0,tq1,tq2]⊗

as in the external notation for programs.  We also add the function 
symbols qequal, qqat, qqn, qnot, qand, qor corresponding to external notation.
The axioms characterizing these functions are:

.begin nofill turnon "∂"
.n←8

$IF:    ∂(n)⊗⊗∀x y z: [qif x qthen y qelse z] = IF x ≠ qNIL THEN y ELSE z⊗
$EQUAL:	∂(n)⊗⊗∀x y: [x qequal y] = IF [x = y] THEN qT ELSE qNIL⊗
$ATOM:	∂(n)⊗⊗∀x: qat x = IF ATOM x THEN qT ELSE qNIL⊗
$NULL:  ∂(n)⊗⊗∀x: qn x = IF NULL x THEN qT ELSE qNIL⊗
$NOT:	∂(n)⊗⊗∀x: qnot x = qif x qthen qNIL qelse qT⊗
$AND:   ∂(n)⊗⊗∀x y: [x and y] = qif x qthen y qelse qNIL⊗
$OR: 	∂(n)⊗⊗∀x y: [x or y] = qif x qthen x qelse y⊗
.end

	For purposes of talking about LISP programs we define the subclass
of terms in our language known as LISP term.
Variables and S-expression constants are LISP terms.  
If ⊗f is one of the basic LISP functions qqa, qqd, qcons, 
qequal, qqat, qqn, qnot, qand, or qor, or the name of a function
representing a LISP program, or a "new" function symbol and the arity
of ⊗f is ⊗n, and ⊗⊗tq0,_tq1,_..._,tq-⊗ are LISP terms then 
⊗⊗f[tq1,_..._,tq-]⊗ and ⊗⊗[λxq1_..._xq-:_tq0][tq1,_..._,tq-]⊗ are
LISP terms.  And those are all the LISP terms.  Notice that
these correspond to the terms of LISP program definitions 
omitting the label construct and programs as arguments.

The restriction to S-expression constants may seem vacuous now,
as those are all we have mentioned so far, but but there will be more.


.ss(total,Representing programs known to terminate.)

	Now we are ready to explain how (some) LISP programs can
be represented.  
First we consider only programs known to terminate.  
There are several syntactic criteria defining classes of such programs.  
They are said to terminate on form.  
We will consider three forms: list recursion, S-expression recursion and 
numeric recursion.   They include a large number of
useful programs and the forms are easy to recognize.
We give some simple examples to illustrate the basic style and method of proof.
Later we will show how to represent programs not known to terminate,
and how to prove termination in some cases.  We will be able to
prove termination of the classes of programs discussed in this section,
so this will turn out to be a special case of the more general method.
We start with the special case as it is easier to explain and allows
us to get to the proving part with less fuss.

	Consider a LISP program given by a definition of the form

!eqntau ⊗⊗⊗f[x]←qt[f,x]       ⊗

where qt is a LISP term involving the variable ⊗x, the program name ⊗f and 
the basic LISP programs S-expression constants and perhaps names
of previously defined programs.   (See qsect{subsection lispth} for more
complete definition of LISP term.)__
This program partially defines a function
also called ⊗f, on S-expressions such that whenever ⊗x is such that the
program terminates with result ⊗y then ⊗⊗f_x=y⊗.
Using the rules for computation given in Chapter {SECTION READIN} 
we can see that for ⊗x such that the computation of ⊗f[x] terminates
we have ⊗⊗f[x]_=_qt[f,x].⊗  Due to the double use of symbols
as external notation for programs and to denote functions in our theory,
and the manner in which the basic LISP function were axiomatized, this
equation holds whether it is viewed as an equation between program terms
or as an equation in the logic (for those ⊗x such  that the computation 
halts).  Thus, given a domain on which the program ⊗f is known to terminate
there is a function ⊗f completely characterized on that domain by the
functional equation corresponding to {eqn tau}.  We can add a new 
function symbol to the language naming this function and the axiom
obtain from {eqn tau} by replacing "←" by "=", replacing the
function parameter by the new function symbol and universally quantifying
over ⊗x.  Clearly this reasoning applies to programs with more than
one input parameter.

	In Chapter {SECTION WRITIN} we discussed various forms of recursive 
definitions.   Some of these forms we claimed had the property that any program
having that form terminates for all allowed input.  One such form was
list recursion: 

!eqntau2a ⊗⊗⊗f[u,qx] ← qif qn u qthen g[qx] qelse h[qa u, qd u, qx, f[qd u, j[qa u, qd u, qx]]]⊗.

The symbols ⊗g, ⊗h and ⊗j  occuring in these definitions must denote
programs definable in terms of previously defined programs (or basic programs),
must be known to terminate on appropriate domains with appropriate ranges.
In particular if  
⊗g terminates on input in domain ⊗⊗Dq0⊗ returning results in ⊗⊗Dq1⊗, 
⊗j terminates on input in ⊗⊗SEXP_qcross_LIST_qcross_Dq0⊗ returning results in 
⊗⊗Dq0⊗ and ⊗h terminates on input in ⊗⊗SEXP_qcross_LIST_qcross_Dq0_qcross_Dq1∪Dq2⊗ 
returning results in ⊗⊗Dq2⊗ then
the program ⊗f will terminate returning results in ⊗⊗Dq1⊗ on arguments in
⊗⊗NULL_qcross_Dq0⊗ and in ⊗⊗Dq2⊗ for arguments in ⊗⊗NELIST_qcross_Dq0⊗.

[Remark:
For simplicity we have included just a single parameter qx in each of the
above forms.  In general we allow any number of parameters (including none)
to appear, and they may be restricted to whatever domains we know about.]

For such a program, if the programs ⊗g, ⊗h, ⊗j are represented by functions
⊗gg, ⊗hh, ⊗jj then we will have the domain mappings:
.begin nofill turnon "∂" 
.group
.n←20

∂(n)⊗⊗gg: Dq0 → Dq1⊗
∂(n)⊗⊗jj: SEXP qcross LIST qcross Dq0 → Dq0⊗
∂(n)⊗⊗hh: SEXP qcross LIST qcross Dq0 qcross D → Dq2⊗
.apart

and if ⊗ff is the function representing ⊗f we will add the domain mappings

.group
∂(n)⊗⊗ff: LIST qcross Dq0 → Dq1 ∪ Dq2⊗
∂(n)⊗⊗ff: NULL qcross Dq0 → Dq1⊗
∂(n)⊗⊗ff: NELIST qcross Dq0 → Dq2⊗
.apart

and the axiom characterizing ⊗ff will be:

⊗⊗⊗∀u qx: ff[u,qx]=qif qn u qthen gg[qx] qelse hh[qa u,qd u,qx, 
ff[qd u,jj[qa u,qd u,qx]]]⊗.

where qx ranges over ⊗⊗Dq0⊗.
.end
.xgenlines←xgenlines-2

	The progam for ⊗append has the form of a list recursion.

$APPEND: __⊗⊗u*v ← qif qn u qthen v qelse qa u . [qd u * v]⊗.

Namely, qx is ⊗v, ⊗⊗Dq0,Dq1,Dq2⊗ are ⊗LIST, ⊗g is the identity,
⊗j returns its third argument and ⊗h[x,w,v,u] is ⊗⊗x_._u⊗.
which has range ⊗NELIST.  Note that if ⊗v is replace by ⊗vv then
all of the component programs return values in ⊗NELIST.  
We can thus introduce the function also denoted by infix * by
giving the domain mappings and equational axiom as follows:
.begin nofill turnon "∂"
.group
.n←20

∂(n)⊗⊗*: LIST qcross LIST → LIST⊗
∂(n)⊗⊗*: NULL qcross LIST → LIST⊗
∂(n)⊗⊗*: NELIST qcross LIST → NELIST⊗
∂(n)⊗⊗*: LIST qcross NELIST → NELIST⊗
.apart

and the axiom characterizing ⊗ff will be:

$APPEND-DEF: __⊗⊗∀u v: u*v = qif qn u qthen v qelse qa u . [qd u * v]⊗.
.end

Two immediate consequences of the defining axiom are:
.begin nofill 
.group

$APPEND-NIL: __⊗⊗∀v: qnil*v = v,     ⊗
$APPEND-UU: __⊗⊗∀uu v: uu*v = qa uu_._[qd uu *v],     ⊗
.end

To prove $APPEND-NIL we substitute qNIL for ⊗u in 
$APPEND-DEF and use the axioms $NULL and $IF.  Thus
.begin nofill turnon "∂"
.m←10 n←50
.group

∂(m)⊗⊗qNIL*v=qif qn qnil qthen v qelse qa qNIL . [qd qNIL * v]⊗∂(n); $APPEND-DEF 
∂(m)⊗⊗______=qif qT qthen v qelse qa qNIL_._[qd qNIL * v]⊗∂(n); $NULL 
∂(m)⊗⊗______= v ⊗∂(n); $IF 
.end

The proof of $APPEND-UU is similar.  Here we need to know that
⊗⊗∀uu: ¬NULL uu⊗ which is a consequence of the domain facts
⊗⊗uu ε NELIST⊗ and ⊗⊗NULL ∩ NELIST = qEMPTY⊗.
.begin nofill turnon "∂"
.m←10 n←50
.group

∂(m)⊗⊗uu*v=qif qn uu qthen v qelse qa uu . [qd uu * v]⊗∂(n); $APPEND-DEF 
∂(m)⊗⊗______=qif qNIL qthen v qelse qa uu_._[qd uu * v]⊗∂(n); $NULL and domain facts
∂(m)⊗⊗______= qa uu_._[qd uu * v] ⊗∂(n); $IF 
.end

In what follows we will not continue to give proofs of such elementary
facts, but just state them as immediate corollaries of the defining axiom.

	The main reason for restricting the second argument of ⊗append to
⊗LIST is that the intent is to stick two lists together to get a new one.
Also, when so restricted the function has nice mathematical properties.

.begin nofill 
.group

$RID-APPEND: __⊗⊗∀u: u*qnil = u,     ⊗
$ASSOC-APPEND: __⊗⊗∀u v w: u*[v*w] = [u*v]*w⊗.
.end

$APPEND-NIL and $RID-APPEND express the fact is that qnil is the "zero" of
the append operation.  The standard mathematical terminology is to say
that qnil is both a left identity and a right identity for ⊗append.  
$ASSOC-APP expresses the fact that ⊗append is associative - like
addition and multiplication of numbers.  [Unlike addition and
multiplication of numbers, ⊗append is not commutative, since $$(A_B)$*$$(C_D)$ =
$$(A_B_C_D)$ ≠ $$(C_D)$*$$(A_B)$].  Associativity allows us to omit brackets and
write ⊗u*v*w, because it doesn't matter how the expression is
parenthesized.

	The proofs of $APPEND_NIL, and $APPEND_UU were untypically easy.
As we remarked in qsect {subsection sexpth} not many interesting general
properties about S-expressions or lists can be proved 
just by substituting in function definitions and using known
properties of S-expressions and the elementary LISP functions.
In fact, when we want to prove something about a function defined by recursion, 
we almost always have to use some corresponding induction principle to carry out 
the proof.  Proving that qNIL is a right identity ($$RID-APPEND$) is an example.
The induction principle corresponding to list recursion is list induction.
Recall that list recursion divides the computation into two cases.  In the
first case the recursion argument is qNIL and the result is computed directly
from the parameters.  In the second case the recursion argument is a non-empty
list ⊗uu and the result can be computed directly once it is known for ⊗⊗qd uu⊗
Similarly to prove a property ⊗⊗qP[u]⊗ using list induction we consider two cases.
In the first case ⊗u is qNIL and we must prove ⊗⊗qP[qNIL]⊗ using facts
and definitions already known.  In the second case ⊗u an a non-empty list ⊗uu and
we prove ⊗⊗qP[uu]⊗ using in addition to known facts, the induction hypothesis
⊗⊗qP[qd uu]⊗.   This analysis is expressed in the schema $LISTINDUCTION given
in qsect {subsection lispth}.   It can also be viewed as a proof rule.

	Let's see how this works to prove ⊗⊗qP_u_≡_u*qNIL=u⊗.  In the NIL case 
we must prove ⊗⊗qNIL*qNIL=qNIL⊗, which is an instance of $APPEND-NIL.  
In the non-NIL case we have the induction hypothesis ⊗⊗qd uu*qNIL = qd uu ⊗, and
.begin nofill turnon "∂" group
.m←10 n←50

∂(m)⊗⊗__uu*qNIL = qa uu_._[qd uu * qNIL]⊗∂(n); $APPEND-UU 
∂(m)⊗⊗__________= qa uu_._qd uu⊗
∂(m)⊗⊗__________= uu ⊗∂(n); $CONS 
.end

which is the desired proof of ⊗⊗qP[uu]⊗ assuming ⊗⊗qP[qd uu]⊗.

	A similar (though slightly more complicated) argument
will prove the associativity of ⊗append ($$ASSOC-APPEND$). 
In particular we want to prove ⊗⊗qP_u_≡_u*[v*w]=[u*v]*w⊗.  
In the NIL case we must prove ⊗⊗qNIL*[v*w]=[qNIL*v]*w⊗, 
which follows easily using two applications of $APPEND-NIL.  
In the non-NIL case we must prove ⊗⊗uu*[v*w]=[uu*v]*w⊗.  We assume
the induction hypothesis: ⊗⊗qd uu*[v*w]=[qd uu*v]*w⊗
We also need the two simple facts
.begin nofill group

$APPEND-CAR: __⊗⊗qa [uu * v] = qa [qa uu_._[qd uu]*v] = qa uu⊗
$APPEND-CDR: __⊗⊗qd [uu * v] = qd [qa uu_._[qd uu]*v] = [qd uu]*v⊗
.end

which are direct consequences of $APPEND-UU, domain facts and the S-expression
facts $CAR and $CDR.  We have
.begin nofill  turnon "∂" group
.m←2 n←50

∂(m)⊗⊗uu*[v*w]=qa uu_._qd uu*[v*w]⊗ ∂(n); $APPEND-UU 
∂(m)⊗⊗________=qa uu_._[[qd uu*v]*w]⊗ ∂(n); induction hypothesis
∂(m)⊗⊗________=qa [uu*v]_._[qd [uu*v]*w]⊗ ∂(n); $APPEND-CAR,CDR 
∂(m)⊗⊗________=[uu*v]*w]⊗ ∂(n); $APPEND-UU 
.end

completing the proof of $ASSOC-APPEND.  The algebra of this proof is rather typical. 
We used the definition of the function involved several times, 
we used the induction hypothesis once, 
and we used the elementary algebraic facts about conditional
expressions and the basic functions of LISP.
Also in this proof it does not matter whether we take ⊗⊗qP[u]⊗ to be
⊗⊗u*[v*w]=[u*v]*w⊗ or ⊗⊗∀v w:u*[v*w]=[u*v]*w⊗.  The difference being that
in the first case the induction hypothesis is only refers to the particular
⊗v and ⊗w of the conclusion while in the second case it applies to any
lists ⊗v, ⊗w.  When proving properties of recursively defined functions,
the unquantified form of qP is generally good enough when the 
function definion does not modify the parameters (non-recursion arguments) in
recursive calls.  If it passes functions of the parameters in recursive
calls then it may be necessary to use the quantified version of qP.

.skip

.cb Exercises.
.item←0

Recall that ⊗reverse and ⊗reverse1 are defined by

	⊗⊗reverse1 u ← if qn u qthen qNIL qelse [reverse1 qd u] * <qa u>⊗

	⊗⊗reverse u ← rev[u, qNIL]⊗

	⊗⊗rev[u, v] ← qif qn u qthen v qelse rev[qd u, qa u . v]⊗

Show that the programs ⊗reverse1 and ⊗rev have the form of list recursion
and give the domain mappings and axioms for the corresponding functions.

Prove the following properties of ⊗reverse   

#. 	⊗⊗∀u: reverse u = reverse1 u⊗

#.	⊗⊗∀u v: reverse[u * v] = [reverse v] * [reverse u]⊗

#.  	⊗⊗∀u: reverse reverse u = u⊗.


The first proof requires inventing a suitable sentence on which to do an
induction.

	Now we consider two other classes of programs that terminate on form.  
Namely, those defined by S-expression rescursion and those defined
by numerical recursion.  (The latter is generally known as primitive recursion.)__
Recall from Chapter_{section WRITIN} that S-expression recursion has the form

!eqntau3 ⊗⊗⊗   f[x,y] ← qif qat x qthen g[x,y] qelse h[qa x,qd x,y,f[qa x,ja[qa x,qd x,y]],
f[qd x,jd[qa x,qd x,y]]]⊗

and numerical recursion has the form

!eqntau1 ⊗⊗⊗f[n,y] ← qif n qequal $0 qthen g[y] qelse h[n-$$1$,y,f[n-$$1$,j[n-$$1$,y]]]⊗.

As for list recursion, the symbols ⊗g, ⊗h, ⊗j, ⊗ja, ⊗jd occuring in these 
definitions must be denote explicitly definable programs 
known to terminate on appropriate domains and having suitable ranges.
In particular for S-expression recursion, if the programs ⊗g, ⊗h, ⊗ja, ⊗jd 
are represented by functions ⊗gg, ⊗hh, ⊗jja, ⊗jjd and we will have the 
domain mappings:
.begin nofill turnon "∂" 
.n←20
.group

∂(n)⊗⊗_gg: SEXP qcross Dq0 → Dq1⊗
∂(n)⊗⊗_hh: SEXP qcross SEXP qcross Dq0 qcross D qcross D → Dq2⊗
∂(n)⊗⊗jja: SEXP qcross SEXP qcross Dq0 → Dq0⊗
∂(n)⊗⊗jjd: SEXP qcross SEXP qcross Dq0 → Dq0⊗
.apart
.group

and if ⊗ff is the function representing ⊗f then we add the domain mappings

∂(n)⊗⊗ff: SEXP qcross Dq0 → Dq1 ∪ Dq2⊗
∂(n)⊗⊗ff: ATOM qcross Dq0 → Dq1⊗
∂(n)⊗⊗ff: PAIR qcross Dq0 → Dq2⊗
.apart
.group

and the axiom characterizing ⊗ff will be:

⊗⊗⊗∀x qx:ff[x,qx]=qif qat x qthen gg[x,qx] qelse 
hh[qa x,qd x,qx,ff[qa x,jj1[qa x,qd x,qx]],ff[qd x,jj2[qa x,qd x,qx]]]⊗.

where qx is of sort ⊗⊗Dq0⊗.
.end

and in the case of numeric recursion, we will have the domain mappings:
.begin nofill turnon "∂"
.n←20
.group

∂(n)⊗⊗gg: Dq0 → Dq1⊗
∂(n)⊗⊗hh: NATNUM qcross Dq0 qcross D → Dq2⊗
∂(n)⊗⊗jj: NATNUM qcross Dq0 → Dq0⊗
.apart
.group

and if ⊗ff is the function representing ⊗f we will add the domain mappings

∂(n)⊗⊗ff: NATNUM qcross Dq0 → Dq1 ∪ Dq2⊗
∂(n)⊗⊗ff: ZERO qcross Dq0 → Dq1⊗
∂(n)⊗⊗ff: POSP qcross Dq0 → Dq2⊗
.apart
.group

and the axiom characterizing ⊗ff will be:

⊗⊗⊗∀n qx:ff[n,qx]=qif n qequal $0 qthen gg[qx] qelse hh[n-$$1$,qx,ff[n-$$1$,jj[n-$$1$,qx]]⊗.

where qx is of sort ⊗⊗Dq0⊗.
.end
.xgenlines←xgenlines-2

[Remark:  
As with list recursion, we have formulated S-expression and numeric recursion
with a single parameter.  The extension to several parameters should be clear.]

.cb Example

	To illustrate the use of the S-expression recursion principle,
we will introduce functions ⊗size, ⊗fringe and ⊗length representing the
programs of the same names and prove 

⊗⊗⊗∀x: length fringe x = size x⊗

(We assume at this point that "+" and simple properties
of numbers are known and will mainly concentrate on techniques for proving
facts about functions on lists and S-expressions.)   

Recall the programs for ⊗size, ⊗fringe and ⊗length: 
.begin nofill turnon "∂" group
.n←10

$SIZE: ∂(n)⊗⊗size x ← qif qat x qthen $1 qelse size qa x + size qd x⊗,
$FRINGE: ∂(n)⊗⊗fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x⊗,
$LENGTH: ∂(n)⊗⊗length u ← qif qn u qthen $0 qelse $$1$ + length qd u⊗
.end

⊗size and ⊗fringe are defined by S-expression recursion and ⊗length by list
recursion.  The domain mappings and axioms for the corresponding functions are:

.begin nofill turnon "∂"
.n←20
.group

$SIZE-DEF: ∂(n)⊗⊗∀x: size x  = qif qat x qthen $1 qelse size qa x + size qd x⊗
	   ∂(n)⊗⊗size: SEXP → POSP⊗
.apart
.group

$FRINGE-DEF: ∂(n)⊗⊗∀x: fringe x = qif qat x qthen <x> qelse fringe qa x * fringe qd x⊗
             ∂(n)⊗⊗fringe: SEXP → NELIST⊗
.apart
.group

$LENGTH-DEF: ∂(n)⊗⊗∀u: length u = qif qn u qthen $0 qelse $$1$+length qd u⊗
             ∂(n)⊗⊗length: LIST → NATNUM⊗
             ∂(n)⊗⊗length: NULL → ZERO⊗
             ∂(n)⊗⊗length: NELIST → POSP⊗
.end

As immediate corollaries of the definitions we have
.begin nofill turnon "∂"
.n←20

.group
$SIZE-ATOM: ∂(n)⊗⊗∀a: size a  = $1 ⊗
$SIZE-PAIR: ∂(n)⊗⊗∀xx: size xx  = size qa xx + size qd xx⊗
.apart
.group

$FRINGE-ATOM: ∂(n)⊗⊗∀a: fringe a = <a> ⊗
$FRINGE-PAIR: ∂(n)⊗⊗∀xx: fringe xx = fringe qa xx * fringe qd xx⊗
.apart
.group

$LENGTH-NIL: ∂(n)⊗⊗length qNIL = $0 ⊗
$LENGTH-UU: ∂(n)⊗⊗∀uu: length uu = $$1$ + length qd uu⊗
.end

Since the definitions of ⊗fringe and ⊗size are S-expression recursions, 
S-expression induction is appropriate to carry out the proof.  
(Recall the rule for S-expression induction given in qsect {subsection sexpth}.)__
We wish to prove ⊗⊗∀x:_qP_x⊗ where:

⊗⊗⊗qP[x] ≡ [length fringe x = size x].           ⊗

In the ATOM case we must prove ⊗⊗∀a: length fringe a = size a⊗. 
We have
.begin nofill turnon "∂" group
.l←8; m←16; n←36;

∂(l)⊗⊗length fringe a = length <a> ⊗  ∂(n) by $FRINGE-ATOM 
	∂(m)⊗⊗= $$1$+length qd <a> ⊗  ∂(n) by $LENGTH-UU and domain facts
	∂(m)⊗⊗= $$1$+length qnil ⊗  ∂(n) by $CDR 
	∂(m)⊗⊗= $1 ⊗ ∂(n) by $LENGTH-ZERO and properties of +. 
	∂(m)⊗⊗= size a ⊗  ∂(n) by $SIZE-ATOM 
.end

which proves the ATOM case.  
In the non-ATOM case we assume the induction hypothesis:

⊗⊗⊗[length fringe qa xx = size qa xx] ∧ [length fringe qd xx = size qd xx]⊗

and prove ⊗⊗length fringe xx = size xx⊗.  We have:
.begin nofill turnon "∂" group
.l←8; m←12; n←50;

∂(l)⊗⊗length fringe xx = length[fringe qa xx * fringe qd xx]⊗  ∂(n) by $FRINGE-PAIR 
and
∂(l)⊗⊗size xx = size qa xx + size qd xx ⊗ ∂(n) by $SIZE-PAIR 
	∂(m)⊗⊗= [length fringe qa xx] + [length fringe qd xx]⊗ ∂(n) by induction hypohesis
.end

By the domain facts ⊗⊗fringe qa xx⊗ and ⊗⊗fringe qd xx⊗  are of sort ⊗LIST, so
we are reduced to proving something of the form ⊗⊗length[u*v]=length_u_+_length_v⊗.
This suggests that we prove a general lemma to that effect and
then the proof will be complete.  We prove

⊗⊗⊗∀u v:[length[u*v]=length u + length v].      ⊗ 

Since the definition of ⊗append is by list recursion we will use 
list induction for the proof.   In the NIL case we must show 

⊗⊗⊗∀v:[length[qNIL*v]=length qNIL + length v].      ⊗ 

We have
.begin nofill turnon "∂" group
.l←8; m←16; n←48;

∂(l)⊗⊗length[qNIL*v] = length v ⊗  ∂(n) by $APPEND-NIL 
	∂(m)⊗⊗= $0 + length v ⊗ ∂(n) by properties of $0 and "+".
	∂(m)⊗⊗= length qnil + length v ⊗ ∂(n) by $LENGTH-NIL. 
.end

proving the NIL case.  In the non-NIL case we assume the induction hypothesis

⊗⊗⊗length [qd uu]*v = length qd uu + length v⊗

and prove ⊗⊗length[uu*v]=length uu+length v⊗.  Thus
.begin nofill turnon "∂" group
.l←8; m←16; n←48;

∂(l)⊗⊗length[uu*v] = $$1$+length qd [uu*v]⊗ ∂(n) by $LENGTH-UU and domain facts
	∂(m)⊗⊗= $$1$ + length [qd uu]*v ⊗ ∂(n) by $APPEND-CDR 
	∂(m)⊗⊗= $$1$ + [length qd uu + length v]⊗ ∂(n) by induction hypothesis.
	∂(m)⊗⊗= length uu + length v⊗ ∂(n) by associativity of + and $LENGTH-UU 
.end
this completes the proof of the lemma and thus of the original theorem.

	As we mentioned earlier, there are many programs that terminate
for all allowed input, but do not fit into one of the standard forms
we have given so far.  We could give more general forms.
[A particularly nice example can be found in Boyer and Moore[1978]].
Instead we will generalize our technique to provide a method
of representing programs defined by a general recursion and
show how to prove termination.


.skip 2
.cb  Exercises
.item←0

.group
#.  You were asked to write definitions for the function
⊗mirror in the exercises of Chapter {subSECTION WRITINex!}.  
Use the previously given definitions of ⊗fringe and ⊗reverse 
(and any facts proved about them so far) to show that your program
satisfies

⊗⊗⊗∀x:[reverse fringe x = fringe mirror x]⊗.

.apart
.ss(partial,Representing programs not known to terminate.)

	The method of the preceding section for representing programs
known to terminate works well and could be extended to cover a large
class of programs.  
However it is not possible to give a syntax that allows exactly
those programs that always terminate, because deciding whether
a program terminates is one of the famous unsolvable problems.
Also, it is well known that LISP programs do not always terminate.  
(You have probably written a few such programs yourself!)  
Many interesting programs terminate on some but not all values of the
arguments (for example ⊗⊗eval⊗) and we would like to be able to say things
about these programs.  
In this section we will show how LISP programs defined by a
general recursion schema can be represented and how termination can
expressed and proved.  
The method extends the method of representing terminating programs.

	Recall the general form of LISP program given in the previous section

!eqngentau ⊗⊗⊗f[x]←qt[f,x]       ⊗


where qt is a LISP term involving ⊗f as a "new" program name.
Let ⊗f also denote the partial function computed by this program.
Thus ⊗⊗f_x=y⊗ for those ⊗x such that the program terminates with result ⊗y. 
Also, for such ⊗x the equation ⊗⊗f_x_=_qt[f,x]⊗  holds as an equation among
program terms and as an equation in the theory if ⊗f is interpreted as
any function agreeing with the program whenever it halts.
Since first order logic has the built in
assumption that a function has a unique value for each of value of its
argument, we can't represent the program by a partial
function on S-expressions directly.  Suppose we try to choose a total
function on S-expressions extending the partial function
and satisfying the the functional equation.  
The following example shows that this is not generally possible.

.bb Omega example: S-expressions aren't enough.

	Consider the program ⊗omega defined by:

$OMEGA: ⊗⊗⊗omega x ← omega x . qNIL⊗.

It is easy to see that this program never terminates.  (In a computer you
would probably get an overflow of some kind as the evaluator attempted
to construct an infinite tree of qNILs. )   Suppose we now form the
corresponding equation

!eqnomegadef ⊗⊗⊗omega x = omega x . qNIL⊗.

and further assume that we can assign  S-expression values to ⊗omega[x] 
such that the equation is satisfied.  
Thus by $CAR and substitution we have ⊗⊗qa omega_x=omega_x⊗.  
But this contradicts the theorem $NO-RPLACS proved in qsect{subsection SEXPTH}.

	Among other things this tells us that if we are to represent
programs by functions satisfying the functional equation, we must
have objects in the domain other than S-expressions.  What we need are
non-S-expression objects to assign as values of the function when the
program doesn't terminate.  It turns out that one additional object
will do.  Thus we extend the domain of S-expressions by adding
the non-Sexpression object qb, called "bottom".  The extended domain will 
be denoted ⊗ESEXP.  The value qb will be assigned to ⊗⊗f_x⊗
when ever the corresponding computation does not terminate.
We extend the basic LISP functions qqa, qqd, qcons, qequal, qqat, qqn, qnot
to ⊗ESEXP by requiring the value to be qb if any of the arguments is qb.
We also require functions representing programs to have the value qb
if any of the arguments is qb.  This corresponds to "call by value"
evaluation which is what LISP does for programs defined in the
manner described in previous chapters.  It is also known as the
"strict" extension.  Other extensions will work, but we won't
treat them here.   The only non-strict functions we have are qif
qand and qor.  qif is qb if its first argument is qb, but no restriction is
made on the second and third arguments.  This represents the specification
that qif only evaluates one of the second or third arguments depending on
the outcome of the evaluating the first argument.
qand, and qor, are extended by extending their definitions in terms of qif. 

[Remark:  A complete description of the theory of extended S-expressions,
and LISP programs is collected in the last section of this chapter.]

	Given the program {eqn gentau} the representing function ⊗f has
the following properties:

(i)  ⊗⊗f X = qt[f,X]⊗ for all arguments.   

(ii)  ⊗f is the "least defined" such function.  That is, if ⊗g is any other 
function satisfying (i), then whenever ⊗⊗f_X⊗ is defined (eg. not qb) 
then ⊗⊗g_X⊗ is also defined and ⊗⊗f_X_=_g_X⊗.

(iii) ⊗⊗f_x=y⊗ for some S-expression ⊗y if and only if 
the program ⊗f on input ⊗x terminates with result ⊗y.  

If the program always terminates then the equation completely determines
the function.  Otherwise we need to express in the theory the fact 
expressed by (ii).  This is done by a ⊗minimization ⊗schema which will
be described later.
If we can prove that ⊗⊗SEXP_f_x⊗  using only the
functional equation and other previously known facts, then we will have
shown that the program terminates on input ⊗x.  

.xgenlines←xgenlines-2

	To summarize we represent a program defined by the recursion
schema {eqn gentau} by function on the domain ⊗ESEXP whose value 
is that determined by the program when it terminates and qb otherwise.
This function is partially characterized by adding the axiom obtained from
the functional equation by quantifying over the intended domains
of definition and adding the domain mappings requiring that the
value be qb if any of the arguments are.  The characterization
is completed by addition of the minimization schema for the recursion
equation.

	We can further generalize the form of definition by allowing 
multiple arguments and/or mutually recursive definitions.  Thus programs
.begin nofill turnon "∂" group
.n←24; m←32

∂(n)⊗⊗fq1[xq1, ... xq-] ← qtq1[fq1, ... ,f%4m%*,xq1, ... ,xq-]⊗
∂(m).
!eqntautau ∂(m).
∂(m).
∂(n)⊗⊗f%4m%*[xq1, ... xq-] ← qt%4m%*[fq1, ... ,f%4m%*,xq1, ... ,xq-]⊗
.end
where the qt%4i%* are LISP terms involving the ⊗⊗f%4i%*⊗ as
new program names are represented by adding to the theory 
new function symbols nameing the programs, 
axioms and domain mappings corresponding to the 
program definitions and an appropriate minimization schema.

.bb Example: Termination and correctness of ⊗⊗flatten⊗.

	As an example of the method we represent the program ⊗flatten, 
which was advertised to compute the fringe of an S-expression, prove
that it is terminates for all S-expressions and show that ⊗flatten 
does indeed compute the same function as ⊗fringe.  The latter proof will 
show how to treat programs defined explicitly in terms of an auxiliary 
program that uses additional parameters.  Recall the definitions
.begin nofill turnon "∂"
.n←15
.group

$FLATTEN: ∂(n)⊗⊗flatten[x] ← flat[x, qNIL]		⊗
$FLAT: ∂(n)⊗⊗flat[x,u] ← qif qat x qthen x.u qelse flat[qa x,flat[qd x,u]]]⊗.
.apart
.group

We add to our theory the axioms

$FLATTEN-DEF: ∂(n)⊗⊗∀x:flatten[x] = flat[x, qNIL]⊗
$FLAT-DEF: ∂(n)⊗⊗∀x u:flat[x,u] = qif qat x qthen x.u qelse flat[qa x,flat[qd x,u]]⊗.
           ∂(n)⊗⊗flat: BOTTOM qcross ESEXP → BOTTOM⊗
           ∂(n)⊗⊗flat: ESEXP qcross BOTTOM → BOTTOM⊗

.apart
.group
and as immediate corollaries we have

$FLAT-ATOM: ∂(n)⊗⊗∀a u:flat[a,u] = a_._u⊗.
$FLAT-PAIR: ∂(n)⊗⊗∀xx u:flat[xx,u] = flat[qa xx,flat[qd xx,u]]⊗
.end

First we will prove 

⊗⊗⊗∀x u: NELIST flat[x,u].              ⊗   

This tells us that the progam for ⊗flat terminates for all input pairs ⊗[x,u] and 
further that the range is the domain ⊗NELIST.  
Since the definition is an extended form of S-expression recursion we try 
S-expression induction as a method of proof.  

In the ATOM case we have ⊗⊗∀a u: NELIST flat[a,u]⊗  by $FLAT-ATOM and the 
domain mappings for qcons.  In the non-ATOM case, we have the induction 
hypothesis

⊗⊗⊗∀u: NELIST flat[qa x,u] ∧ ∀u: NELIST flat[qd x,u]⊗.

By $FLAT-PAIR we have ⊗⊗flat[xx,u] = flat[qa xx,flat[qd xx,u]]⊗. Using the 
d-part of the hypothesis we then can apply the a-part with ⊗u replaced
by ⊗⊗flat[qd xx,u]⊗ and this completes the proof.  An immediate consequence
of this proof and $FLATTEN is that ⊗⊗∀x:_NELIST_flatten_x⊗.

	Now we will prove ⊗⊗∀x: flatten x = fringe x⊗.   By $FLATTEN this
is the same as ⊗⊗∀x:_flat[x,qnil]_=_fringe_x⊗.   The simple principles we
have used so far suggest that we proceed directly with a proof by S-expression
induction on ⊗x.  This unfortunately arrives at a dead end.  
(If you had trouble provinge ⊗⊗∀u: reverse1 u=reverse u⊗ this may be why!)
The difficulty is that we begin with the second argument qnil, 
but after expanding the definition once this is no longer the case.  
Just as we have to carry along an extra variable in the computation we 
also do in the proof.  There are several possible routes to take.  
We will prove the following more general statement

⊗⊗⊗∀x u: flat[x,u] = fringe x * u.            ⊗

Clearly the statement we started to prove is a direct consequence of this one.
and now we may proceed by a straightforward S-expression induction.   
In the ATOM case we have:
.begin nofill turnon "∂" group
.l←4;m←12;n←40;

∂(l)⊗⊗flat[a,u] = a . u⊗    ∂(n) by $FLAT-ATOM 
          ∂(m)⊗⊗= <a> * u⊗  ∂(n) by $APPEND-NIL,APPEND-UU, since ⊗⊗<x> = x . qnil⊗.
          ∂(m)⊗⊗= fringe a * u⊗  ∂(n) by $FRINGE-ATOM 
.end
In the non-ATOM case we have the induction hypothesis:

⊗⊗⊗∀u: flat[qa xx,u]_=_fringe qa xx * u ∧ ∀u: flat[qd xx,u] = fringe_qd xx * u⊗. 

and we have
.begin nofill turnon "∂" group
.l←4;m←12;n←40;

∂(l)⊗⊗flat[xx,u] = flat[qa xx,flat[qd xx,u]]⊗  ∂(n); $FLAT-PAIR 
	    ∂(m)⊗⊗= flat[qa xx,fringe qd xx * u]⊗  ∂(n); induction hypothesis
	    ∂(m)⊗⊗= fringe qa xx * [fringe qd xx * u]⊗ ∂(n); induction hypothesis 
	    ∂(m)⊗⊗= fringe xx * u⊗   ∂(n); $ASSOC-APPEND,FRINGE-PAIR  
.end
This completes the proof.
Notice that in order to apply the induction hypothesis and the associativity
of ⊗append it is necessary to check the domain facts for ⊗fringe.  

.bb Example: termination of programs defined by list recursion.

	Suppose we have a program defined by list recursion as follows

$F: __⊗⊗f[u,qx] ← qif qn u qthen g[qx] qelse h[qa u,qd u,qx,f[qd u,j[qa u,qd u,qx]]⊗.

and that the programs ⊗g, ⊗h, and ⊗j  are represented by functions having 
the same names such that we have the domain mappings:
.begin nofill turnon "∂" 
.group
.n←20

∂(n)⊗⊗g: Dq0 → Dq1⊗
∂(n)⊗⊗j: SEXP qcross LIST qcross Dq0 → Dq0⊗
∂(n)⊗⊗h: SEXP qcross LIST qcross Dq0 qcross D → Dq2⊗
.end

where ⊗⊗Dq0,Dq1,Dq2⊗ are domains and ⊗⊗D=Dq1∪Dq2⊗, and qx ranges over ⊗⊗Dq0⊗.
Then the program ⊗f is represented by a function ⊗f satisfying the axiom:

$F-DEF: __⊗⊗∀u qx: f[u,qx]=qif qn u qthen g[qx] qelse h[qa u,qd u,qx,f[qd u,j[qa u,qd u,qx]]⊗.

which has the following immediate corollaries:
.begin nofill group

$F-NIL: __⊗⊗∀qx: f[qNIL,qx]=g[qx]⊗.
$F-UU: __⊗⊗∀uu qx: f[uu,qx]=h[qa uu,qd uu,qx,f[qd uu,j[qa uu,qd uu,qx]]⊗.
.end

Using list induction we can prove ⊗⊗∀u qx:D f[u,qx]⊗.  In the NIL case we have
⊗⊗∀qx:_D_f[qNIL,qx]⊗ by $F-NIL and the domain mappings for ⊗g.  In the non-NIL
case we assume the induction hypothesis ⊗⊗∀qx:_D_f[qd uu,qx]⊗.  By $F-UU we
have ⊗⊗f[uu,qx]=h[qa uu,qd uu,qx,f[qd uu,j[qa uu,qd uu,qx]]]⊗.  Using the
domain mapping for ⊗j and the induction hypothesis we have
⊗⊗D_f[qd uu,j[qa uu,qd uu,qx]]⊗ and using the domain mapping for ⊗h we 
have ⊗⊗D_f[uu,qx]⊗ as desired.   Using this we can easily show the further
domain properties claimed for ⊗f, ⊗⊗∀qx:_Dq1_f[qNIL,qx]⊗ and 
⊗⊗∀uu_qx:_Dq2_f[uu,qx]⊗.   Thus representation of programs defined by list
recursion is a special case of the more general method.
.xgenlines←xgenlines-2
Showing that the S-expression recursion and numeric recursion principles
are also special cases is similar.   We need only replace list induction
by S-expression or numeric induction respectively.


.ss(recpred,Recursively Defined Predicates.)

	In Chapter {SECTION READIN} we introduced propositional constructs
⊗and, ⊗or and ⊗not into the programing language with the intent
that they should behave like the usual logical operators.  
We also treated some of the recursive definitions as though they
defined predicates rather than functions (for example ⊗member and ⊗equal).  
In this section we will show how to represent programs by
recursively defined predicates.   For many programs written using
the propositional constructs there is a corresponding predicate
on S-expressions satisfying the equivalence obtained by replacing
"←" by "≡" and the propositional programs by the corresponding 
logical connectives or predicates.
In general it is not safe to make such a translation directly.
To see why consider the following program:

$LOSE: __⊗⊗lose x ← qnot lose x ⊗.

This would translate into

$LOSE-DEF: __⊗⊗∀x:[lose x ≡ ¬lose x] ⊗.

which clearly loses by leading to a contradiction!
We avoided a similiar problem for function definitions
by adding the element qb to the domain thus providing a non S-expression
value to assign to a term when the computation did not produce a value.
Our solution is here
the following.  We continue to view recursive definitions
as defining functions.  Some of these functions will be intended
to compute predicates in the sense that the predicate is true 
only for those values of the arguments for which the value of the
function is an S-expression other that qNIL.  This is most naturally carried 
out in terms of a predicate ⊗True characterized by the axiom:

$TRUTH: __⊗⊗∀X: [True X ≡ SEXP X ∧ X≠qNIL]⊗

from which we easily deduce

$TRUTH1: __⊗⊗∀x: [True x ≡ x≠qNIL]⊗



	For example consider the recursive program

$SUBEXPF: __⊗⊗subexpf[x, y] ← [x qequal y] qor [qnot qat y qand [subexpf[x, qa y] qor subexpf[x, qd y]]]⊗.

Our intent is to define a predicate ⊗subexp satisfying the equivalence

$SUBEXP: __⊗⊗∀x y: [subexp[x, y] ≡ [x = y] ∨ [¬ATOM y ∧ [subexp[x, qa y] ∨ subexp[x, qd y]]]]⊗,

but we have no rule that allows changing a recursive program immediately
into an equivalence relation for a predicate.  Such a rule would lose as
described above.  Therefore, we first
represent the program as a function obtaining the axiom
.begin nofill group

$SUBEXPF-DEF: ⊗⊗∀x y:subexpf[x,y]=[x qequal y]qor[qnot qat y qand [subexpf[x,qa y] qor subexpf[x,qd y]]]⊗

and the two immediate corollaries:  

$SUBEXPF-ATOM: __⊗⊗∀x a: subexpf[x,a] = x qequal a⊗
$SUBEXPF-PAIR: __⊗⊗∀x yy: subexpf[x,yy] = x qequal yy qor [subexpf[x,qa yy] qor
subexpf[x,qd yy]].⊗
.end

.if false then begin "hide"
This is permissible without first proving the program always terminates,
because, as proved in (Cartwright 1976), the function can consistently be
regarded has taking the value qb when the program doesn't terminate.
.end "hide"

We prove that ⊗subexpf is total 

$S-SUBEXP: __⊗⊗∀x y: SEXP subexpf[x, y].       ⊗

using S-expression induction on the second argument.  Thus we wish to prove 
⊗⊗∀y:_qP_y⊗⊗ where:

⊗⊗⊗qP[y] ≡ ∀z: SEXP subexpf[z,y].              ⊗

This works because recursive calls to ⊗subexpf in the definition all involve
⊗⊗qa y⊗ or ⊗⊗qd y⊗ as the second argument.  
For the ATOM case  ⊗⊗∀z a: SEXP subexpf[z,a]⊗ follows from $SUBEXPF-ATOM 
and the domain mapping of qequal.
In the non-ATOM case we have the induction hypotheses

⊗⊗⊗∀z: SEXP subexpf[z,qa yy] qand ∀z: SEXP subexpf[z,qd yy]⊗

and ⊗⊗∀z: SEXP subexpf[z,yy]⊗ follows from 
this together with $SUBEXPF-PAIR and the domain mappings for qequal and qor.

If we define the predicate ⊗subexp by

$SUBEXP-DEF: __⊗⊗∀X Y: [subexp[X, Y] ≡ True subexpf[X, Y]⊗.

we can prove the original sentence proposed for ⊗subexp.  

	First we give characterizations of the propositional functions in 
terms of the predicate ⊗True and the logical operations and predicates that 
the functions are indended to imitate.  They follow directly from the
defining axioms.
.begin nofill turnon "∂"
.n←20

$EQNOT:        		∂(n)⊗⊗∀x: [True qnot x ≡ ¬True x]⊗
$EQAND: 		∂(n)⊗⊗∀x y: [True[x qand y]≡ [True x ∧ True y]]⊗
$EQOR: 			∂(n)⊗⊗∀x y: [True[x qor y] ≡ [True x ∨ True y]]⊗
$EQEQUAL: 		∂(n)⊗⊗∀x y: [True[x qequal y] ≡ x = y]⊗
$EQATOM: 		∂(n)⊗⊗∀x: [True[qat x] ≡ ATOM x]⊗
$EQNULL: 		∂(n)⊗⊗∀x: [True[qn x] ≡ NULL x]⊗
.end



The proof of $SUBEXP is just a sequence of simplifications based on the
use the $EQ- lemmas, the definitions and the totality of ⊗subexpf.  
In particular, by $SUBEXP-DEF we need only show

⊗⊗⊗∀x y:[True subexpf[x,y] ≡ [x=y] ∨ [¬ATOM y ∧ [True subexpf[x,qa y] ∨ True subexpf[x,qd y]]]]⊗

In the ATOM case by $SUBEXPF-ATOM 

⊗⊗⊗ ∀x a: [True[x qequal a] ≡ x = a]⊗

which is true by $EQEQUAL.  In the non-ATOM case we let ⊗⊗y=yy⊗ and 
by $SUBEXPF-PAIR, $S-SUBEXPF we need only show
.begin nofill

⊗⊗⊗∀x yy: [True [ [x qequal yy] qor [subexpf[x,qa yy] qor subexpf[x,qd yy]] ]⊗
⊗⊗⊗______≡ [x = yy] ∨ True subexpf[x,qa yy] ∨ True subexpf[x,qd yy] ]_____⊗
.end

But this follows from $S-SSUBEXPF, $EQOR, and $EQEQUAL.  

[Remark:
Our method of interpreting functions as predicates
was chosen to correspond with the usual LISP convention.  Other
conventions are possible.  For example we could restrict the functions
that are to be interpreted as predicates to have values in the domain
α{qT, qNIL, qb}.  The axioms for qand etc. would be slightly different,
but not much else changes.  
]


.cb Exercise

	You were asked to write the definition for the predicate ⊗istail in the 
exercises of Chapter_{subSECTION WRITINex!}.  
Prove the following facts about ⊗istail.  
.begin nofill  indent 12,12

⊗⊗∀v: istail[qNIL,v]⊗
⊗⊗∀u v: [¬NULL u ∧ istail[u,v] ⊃ istail[qd u,v]]⊗
⊗⊗∀u v w: [istail[u,v] ∧ istail[v,w] ⊃ istail[u,w]]⊗
.end

First translate your definition of ⊗istail into a functional equation for
the function ⊗istailf.  Show ⊗istailf is total and that ⊗istail satisfies
the equivalence you intended.  All of this parallels the ⊗subexp example
above.  For the rest you are on your own.

.ss(induction, Additional induction principles for proving.)

	When we presented the theory of LISP we introduced
princples of induction for S-expressions, lists, and numbers
based on the structure of the respective domains.  
These principles work well for proving facts about functions
defined by the corresponding recursions.  They are not
generally easy to use when other forms of recursion are used in
the function definition.  In this section we will present some
additional principles of induction.

.bb Induction on well-founded orderings

	The general idea of induction on some domain involves a notion of 
"smaller" on that domain which is ⊗well-founded.  By well-founded we mean
that every sequence of elements in which each element is smaller
than the previous one must terminate after a finite number of steps.
Given a well-founded notion of smaller and a property qP, if it
is the case that whenever qP holds for all elements smaller than
a given element then it also holds for that element, then we have qP
holds for all elements of the domain.  This can be formally expressed
by the schema

⊗⊗⊗∀qx: [∀qxq1: [R[qxq1,qx] ⊃ qP qxq1] ⊃ qP qx] ⊃ ∀qx: qP qx⊗

where ⊗R is a well-founded relation on the domain and qx,qxq1 are variables
ranging over the domain.

	To see that this induction principle is "correct" suppose
the hypothesis holds and suppose there is some qx such that ⊗⊗¬qP_qx⊗.
Then since ⊗R is well-founded, there is a smallest qx such that ⊗⊗¬qP_qx⊗.
Otherwise we could find smaller counter examples ad-infinitum, forming
a nonterminating sequence of elements each of which is smaller 
(as measured by ⊗⊗R⊗) than its predecessor.  This contradicts the
well-foundedness of ⊗R.  If qx is the smallest counter example then
⊗⊗∀qxq1: R[qxq1,qx] ⊃ qP qxq1⊗  therefore ⊗⊗qP qx⊗ must hold
after all.  Hence there is no such counter example.

	As examples of well-founded relations on domains of immediate interest
we have 
.begin nofill group
.indent 10,10

<  the usual order relation on numbers
<%4l%* on lists where ⊗⊗u <%4l%* v ≡ ∃ww: v=ww*u⊗, e.g. ⊗u is a proper tail of ⊗v.  
<%4S%* on S-expressions where ⊗⊗x <%4S%* y ≡ x≠y ∧ subexp[x,y]⊗,
 ________e.g. ⊗x is a proper subexpression of ⊗y.  
.end
.xgenlines←xgenlines-2

Corresponding to these relations we have the following induction schemata:
.begin nofill group turnon "∂"

$NUMBINDUCTION-CVI: ∂(28)⊗⊗∀n: [∀m: [m < n ⊃ qP m] ⊃ qP n] ⊃ ∀n: qP n⊗
$LISTINDUCTION-CVI: ∂(24)⊗⊗∀u: [∀v: [v <%4l%* u ⊃ qP v] ⊃ qP u] ⊃ ∀u: qP u⊗
$SEXPINDUCTION-CVI: ∂(28)⊗⊗∀x: [∀y: [y <%4S%* x ⊃ qP y] ⊃ qP x] ⊃ ∀x: qP x⊗
.end

	Given domains ⊗⊗Dq1⊗ and ⊗⊗Dq2⊗ with well-founded orderings 
<q1, <q2 respectively there are a number of ways to construct new
orderings on combinations of these domains.  For example the
lexicographic ordering <q1q2 on ⊗⊗Dq1_qcross_Dq2⊗ is defined by

⊗⊗⊗(qxq1,qxq2) <q1q2 (qxq1',qxq2') ≡ [qxq1 <q1 qxq1' ∨ [qxq1=qxq1' ∧ qxq2 <q2 qxq2']]⊗

Another means of defining a well-founded ordering is to induce one
by a mapping into a domain that has a well-founded ordering.
Thus if ⊗⊗qrho: Dq1 → Dq2⊗ and  <q2 is a well-founded ordering on ⊗⊗Dq2⊗
then the ordering <%4r%* on ⊗⊗Dq1⊗ defined by 
⊗⊗qx_<%4r%*_qx'_≡_qrho_qx_<q2_qrho_qx'⊗ is well-founded.

.xgenlines←xgenlines-2


.bb Rank functions and Induction on rank.

	Suppose ⊗f is a recursively defined program on some domain ⊗D  
and let qx be a variable of sort ⊗D.  
Suppose further that the recursive calls to ⊗f in the definition
have arguments of the form ⊗⊗gq1_qx,_gq2_qx,_..._gq-_qx⊗.  
If a recursion
is to succeed the recursive calls should be with arguments which are smaller
in some sense.  One way to make the notion of smaller precise is to
find a "rank function " ⊗⊗qrho:_D_→_NATNUM⊗ such that
⊗⊗qrho_g%4i%*_qx_<_qrho_qx⊗ for ⊗⊗1≤i≤n⊗.  This rank function can be
used to prove properties of the function compute by ⊗f using
the principle of "induction on qrho".   
Informally, this principle says that if whenever
⊗⊗qP qxq1⊗ holds for all qxq1 of lesser rank than qx then qx satisfies qP,
then all qx satisfy qP.  
Formally we have the schema:

$RANKIND: ⊗⊗⊗∀qx: [∀qxq1:[qrho qxq1 < qrho qx ⊃ qP qxq1] ⊃ qP qx] ⊃ ∀qx: qP qx⊗

One way to justify the schema is as an instance of induction on a well-founded
ordering.  Namely the ordering <%4r%* defined by 

⊗⊗⊗qxq1 <%4r%* qx ≡ qrho qxq1 < qrho qx⊗

is well-founded.  (Any strictly decreasing <%4r%*_sequence induces
a corresponding strictly decreasing <_sequence.)
It can also be deduced in our theory from an appropriate instance of
$NATNUMINDUCTION-CVI.  Before we prove that, we show how "rank induction"
can be applied.
.xgenlines←xgenlines-2

	Consider the program ⊗gopher defined by

$GOPHER: ____⊗⊗gopher x ← qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗.

We represent this program by the function ⊗gopher satisfying the axiom:
.begin nofill turnon "∂" group
.n←15

$GOPHER-DEF: ____⊗⊗∀x: gopher x = qif qat qa x qthen x qelse gopher [qaa x . [qda x . qd x]]⊗.

which has the immediate consequences:

$GOPHER-ATOM: ∂(n)⊗⊗∀xx: [ATOM qa xx ⊃ gopher xx=xx]⊗
$GOPHER-PAIR: ∂(n)⊗⊗∀xx: [PAIR qa xx ⊃ gopher xx=gopher[qaa xx_._[qda xx_._qd xx]]]⊗
.end


⊗gopher digs up the left most atom of its argument, stacking the d-parts
of successive ⊗⊗car⊗s as it goes.  If you are familiar with operations
on binary trees, ⊗gopher can be viewed as performing successive
clock-wise rotations.  These operations preserve the symmetric order on
leaves of the tree.  This corresponds to preserving the fringe of an
S-expression.  

	From the definition we see that ⊗gopher makes sense only on 
non-atomic S-expressions.  In the recursive call ⊗⊗gopher[qaa x_._[qda x_._qd x]]⊗
we see that what is getting "smaller" is ⊗⊗qa x⊗. In particular

$GOPHER-RANK: ____⊗⊗∀xx: [PAIR qa xx ⊃_size_qa [qaa xx_._[qda xx_._qd xx]]_<_size_qa xx.]⊗

So ⊗⊗qrho_xx=size_qa xx⊗ is an appropriate rank function for proving facts
about gopher.  We will prove the following simple facts:
.begin nofill turnon "∂" group
.n←15

$PAIR-GOPHER: ∂(n)⊗⊗∀xx: PAIR_gopher xx⊗
$SIZE-GOHPER: ∂(n)⊗⊗∀xx: size gopher xx = size xx⊗
.end

To prove ⊗⊗∀xx: PAIR gopher xx⊗ we assume the rank induction hypothesis

⊗⊗⊗∀yy:_[size qa yy<size qa xx ⊃ PAIR gopher yy]⊗

There are two cases corresponding two parts of the definition of ⊗gopher.  
If ⊗⊗ATOM qa xx⊗ then ⊗⊗PAIR gopher xx⊗ follows from $GOPHER-ATOM.  
If ⊗⊗PAIR qa xx⊗ then ⊗⊗PAIR gopher xx⊗ follows from $GOPHER-PAIR,  
$GOPHER-RANK and the induction hypothesis.  This completes the proof of 
$PAIR-GOPHER.  

The proof of ⊗⊗∀xx: size gopher xx = size xx⊗ is similar.  We need a lemma 
about ⊗size:  

⊗⊗⊗∀xx: [PAIR qa xx⊃size xx=size [qaa xx_._[qda xx__qd xx]]]⊗

which follows from $SIZE-PAIR and the associativity of "+".
We assume the rank induction hypothesis

⊗⊗⊗∀yy:_[size qa yy<size qa xx ⊃ size gopher yy=size yy]⊗

If ⊗⊗ATOM_qa xx⊗ then ⊗⊗size_gopher_xx=size_xx⊗ follows from $GOPHER-ATOM.  
If ⊗⊗PAIR_qa xx⊗ then ⊗⊗size_gopher_xx=size_xx⊗ follows from $GOPHER-PAIR,  
$GOPHER-RANK, the size lemma and the induction hypothesis.  
This completes the proof of $SIZE-GOPHER.  

 	We have presented the idea of a rank function taking only one argument
for notational simplicity.   This idea and the corresponding induction
principle generalize easily to multiple arguments.


	To conclude our discussion of induction principles we will show
how $RANKIND can be derived from $NUMBINDUCTION-CVI.  In particular
let ⊗D be some domain, qx, qxq1 variables ranging over ⊗D and 
let qrho be a rank function ⊗⊗qrho:_D_→_NATNUM⊗ and let qQ be a predicate
parameter.  Then we want to prove:

$RANKIND: ____⊗⊗∀qx: [∀qxq1:[qrho qxq1 <qrho qx ⊃qQ qxq1] ⊃ qQ qx] ⊃ ∀qx: qQ qx⊗

We instantiate $NUMBINDUCTION-CVI taking ⊗⊗qP[n]≡∀qx: qrho qx=n ⊃ qQ qx⊗ 
obtaining

$RANK-NUM: ____⊗⊗∀n: [∀m: [m < n ⊃ ∀qx: [qrho qx=m⊃qQ qx]] ⊃ ∀qx: [qrho qx=n⊃qQ qx] ]
⊃ ∀n: ∀qx: [qrho qx=n⊃qQ qx]⊗

To prove $RANKIND we assume 

$RANKHYP: ____⊗⊗∀qx: [∀qxq1:[qrho qxq1 <qrho qx ⊃qQ qxq1] ⊃ qQ qx] ⊗

and show ⊗⊗ ∀qx: qQ qx⊗.  Since the range of qrho is ⊗NATNUM, by $RANK-NUM 
it is sufficient to show 

⊗⊗⊗∀n: [∀m: [m < n ⊃ ∀qx: [qrho qx=m⊃qQ qx]] ⊃ ∀qx: [qrho qx=n⊃qQ qx] ].      ⊗

Thus we assume 

$RNUM-HYP: ____⊗⊗∀m: [m < n ⊃ ∀qx: [qrho qx=m⊃qQ qx]] ⊗

and prove ⊗⊗∀qx: [qrho qx=n⊃qQ qx] ]⊗  Assuming 

$RHO-N: ⊗⊗qrho qx=n⊗

by $RANKHYP,RHO-N it is sufficient to show ⊗⊗∀qxq1:[qrho qxq1 < n ⊃qQ qxq1].⊗
Assuming

$RHO-M: ⊗⊗qrho qx1 < n⊗

by $RNUM-HYP with ⊗⊗m=qrho qxq1⊗  and $RHO-M we have ⊗⊗qQ qxq1⊗ which 
completes the proof.


.<<special cases>>

.cb Exercises
.item ← 0

	#. Prove the following additional properties of ⊗gopher using induction on the
rank.
.begin nofill turnon "∂" group
.n←25

$CAR-GOPHER-FRINGE: ∂(n)⊗⊗∀xx: qa fringe xx = qa gopher xx⊗
$CDR-GOHPER-FRINGE: ∂(n)⊗⊗∀xx: qd fringe xx = fringe qd gopher xx⊗
.end

	#. Derive the schema $SEXPINDUCTTION from the schema $NUMBINDUCTION-CVI 
by devising a suitable rank function.

[Remark:  the point of this exercise and the above proof is to give you
the idea that the various induction principles are just different ways of
saying the same thing.  In a practical proving system it is useful to
have many ways to express various notions.]

.ss(minim,Partial functions and the Minimization Schema.)

	So far we have dealt only with recursive programs that defined 
total functions on S-expressions.   In these cases the functional equation
corresponding to the recursive definition completely characterized the
function on S-expressions.  Frequently we are interested in a program
that does not always terminate and in this case there are likely to 
be many functions that satisfy the corresponding functional equation.
Whatever we prove using this equation will be true
for all of these functions, but there are also facts about the
program we are representing that will not be provable using only
the functional equation.  
For example, the program

!fcnloop&2 ⊗⊗⊗loop x ← loop x			⊗

leads to the sentence

!eqnloopax2 ⊗⊗⊗∀x: [loop x = loop x]		⊗

which provides no information (all functions satisfy it) 
although the function ⊗loop corresponding to the program is undefined for all ⊗x.  
This is not always the case.   Recall the program

!fcnomega&1 ⊗⊗⊗omega x ← [omega x] . qNIL		⊗

which has the functional equation

!eqnomegaax1 ⊗⊗⊗∀x: [omega x = [omega x] . qNIL] .	⊗

We showed in qsect {subsection partial}
that assuming ⊗⊗SEXP omega x⊗ leads to
a contradiction thus we can show
⊗⊗∀x: [¬SEXP omega x]⊗, using the functional equation and induction.

	In order to characterize recursive programs, we need some
way of expressing the fact that the function we mean is
the least defined solution of the functional equation.   We will do
this by introducing, in addition to the functional equation, a
schema called the ⊗minimization_schema which expresses the fact that
every function satisfying the equation on the domain of definition is defined
at least every where that the function assigned to the program is defined,
and when both are defined, the have the same value.

	If the program ⊗f is defined by

!eqnpdef2  ⊗⊗⊗f qx ← qt[f,qx] 		⊗

we have a function ⊗f satisyfying the functional equation

!eqnpdefeq  ⊗⊗⊗∀qx: f qx = qt[f,qx] 	        ⊗

where qx is a variable ranging over the domain ⊗D.  
The minimization schema for this form of recursive definition has the form

!eqnminsch ⊗⊗⊗∀qx: [D qt[F,qx] ⊃ F qx = qt[F,qx]] ⊃ ∀qx: [D f qx ⊃ f qx = F qx] ⊗.

Here ⊗F is a function parameter.   This schema is really ⊗schema_schema, 
since for any particular term qt and function symbol ⊗f we produce
from the schema a formula that still contains the parameter ⊗F.  
We then must substitute some function expression of our language for ⊗F 
to produce an axiom.  (This is similar to the induction schemas, except
there we substituted formulas for predicate parameters.)

	The simplest application of the minimization schema is to show that 
the program for ⊗loop given above computes the totally undefined function.
The minimization schema for loop is

!eqnloopminsch ⊗⊗⊗∀x:[SEXP F x ⊃ F x = F x] ⊃ ∀x: [SEXP loop x ⊃ loop x = F x] ⊗.

If we let ⊗F be the function expression λX: qb then we obtain the axiom

⊗⊗⊗∀x:[SEXP qb ⊃ qb = qb] ⊃ ∀x: [SEXP loop x ⊃ loop x = qb] ⊗.

The left side of the implication is identically true since 
⊗⊗SEXP ∩ BOTTOM = qEMPTY⊗  or ⊗⊗¬SEXP_qb⊗.  Thus we have

⊗⊗⊗∀x: [SEXP loop x ⊃ loop x = qb] ⊗.

If we assume ⊗⊗SEXP loop x⊗ we obtain SEXP qb which is a contradiction.
Thus we have shown 

⊗⊗⊗∀x: ¬SEXP loop x                ⊗

as desired.

	The minimization schema can sometimes be used to show partial
correctness.  For example, the notorious 91-function is defined by
the recursive program over the natural numbers
.begin nofill group

⊗⊗⊗f%491%* n ← qt%491%*[f%491%*,n]                       ⊗
where
⊗⊗⊗qt%491%*[F,n] = qif n > 100 qthen n - 10 qelse F F [n + 11] ⊗.
.end

The corresponding minimization schema is

⊗⊗⊗∀n: [NATNUM qt%491%*[F,n] ⊃ F n = qt%491%*[F,n]] ⊃ 
∀n: [NATNUM f%491%* n ⊃ f%491%* n = F n] ⊗.

.xgenlines←xgenlines-2

The goal is to show that
.begin nofill group

⊗⊗⊗∀n: [f%491%* n = F%491%* n                             ⊗
where
⊗⊗⊗∀n: [F%491%* n = qif n > 100 qthen n - 10 qelse 91] .  ⊗
.end

Using the minization schema we can easily show that

⊗⊗⊗∀n: [NATNUM f%491%* n ⊃ f%491%* n = F%491%* n .	   ⊗

Namely, we need only show

⊗⊗⊗∀n: [NATNUM qt%491%*[F%491%*,n] ⊃ F%491%* n = qt%491%*[F%491%*,n]] ⊗ 

which follows by direct calculation from the definitions of 
⊗⊗F%491%*⊗ and ⊗⊗qt%491%*⊗ by considering the three cases
⊗n>100, ⊗89<n≤100 and ⊗n≤89.  The hypothesis of the implication is not
needed here.

	The older proof method of ⊗recursion ⊗induction (McCarthy 1963) is also
an immediate application of the minimization schema.  If we show
that two functions satisfy the schema of a recursive program, we
show that they both equal the function computed by the program 
wherever the function is defined.

For example we can use the minimization schema for the program 

$REV: __⊗⊗rev[u,v] ← qif qn u qthen qv qelse rev[qd u,qa u_._ v]⊗

and the fact that ⊗⊗∀u_v:_LIST_rev[u,v]⊗ to show that  

$EQ-REV: ⊗⊗∀u:_rev[u,qNIL]=reverse[u] where

$REVERSE: __⊗⊗reverse u ← qif qn u qthen qNIL qelse [reverse qd u]*<qa u>⊗.

The minimization schema for the program ⊗rev is 

⊗⊗⊗∀u v: [LIST qt%4rev%*[F,u,v] ⊃ F[u,v] = qt%4rev%*[F,u,v]] ⊃ 
∀u v: [LIST rev[u,v] ⊃ rev[u,v] = F[u,v]] ⊗.

Taking ⊗⊗F[u,v]=revrse[u]*v⊗, we need only show ⊗⊗F[u,v]=qt%4rev%*[F,u,v]⊗
as this gives ⊗⊗∀u_v:_rev[u,v]=reverse[u]*v⊗ and $EQ-REV is a special case.
By the definitions we need only prove

⊗⊗⊗reverse[u]*v=qif qn u qthen v qelse reverse[qd u]*[qa u_._v]⊗.

In the case ⊗u is qNIL both sides of the equation simplify to ⊗v.  
In the case ⊗u is some non-empty list ⊗uu we by $REVERSE we need only show

⊗⊗⊗ [reverse[qd uu]*<qa uu>]*v=reverse[qd uu]*[qa uu_._v].⊗

But this is an easy consequence of $ASSOC-APPEND,APPEND-NIL,APPEND-UU.  

	The utility of the minimization schema for proving partial
correctness or non-termination depends on our ability to name
suitable comparison functions.  ⊗loop and ⊗⊗f%491%*⊗ were easily treated,
because the necessary comparison functions could be given explicitly
without recursion.  Any extension of the language that provides new
tools for naming comparison functions, e.g. going to higher order
logic, will improve our ability to use the schema in proofs.

.ss(lispax,Theory of LISP: Algebraic Axioms.)
 
	In this appendix we collect the language specification,
domain facts and axioms for the theory of extended S-expressions
and the subdomains of S-expressions, lists and numbers, and
the definitions of functions representing the basic LISP programs.

.bb Domains

⊗ESEXP, ⊗BOTTOM, 
⊗SEXP, ⊗PAIR, ⊗ATOM, 
⊗LIST, ⊗NELIST, and ⊗NULL 
⊗NATNUM, ⊗POSP, and ⊗ZERO.  

.bb Domain relations:

.begin nofill turnon "∂" turnoff "{}"
.n←20
.group

∂(n)⊗⊗ESEXP = SEXP ∪ BOTTOM⊗
∂(n)⊗⊗SEXP ∩ BOTTOM = qEMPTY⊗
.apart
.group

∂(n)⊗⊗SEXP ⊂ ESEXP⊗
∂(n)⊗⊗SEXP = ATOM ∪ PAIR⊗
∂(n)⊗⊗ATOM ∩ PAIR = qEMPTY⊗
.apart
.group

∂(n)⊗⊗LIST ⊂ SEXP⊗
∂(n)⊗⊗NELIST ⊂ PAIR⊗
∂(n)⊗⊗NULL = {qNIL}⊗
∂(n)⊗⊗LIST = NULL ∪ LIST⊗
∂(n)⊗⊗NULL ∩ NELIST = qEMPTY⊗
.apart
.group

∂(n)⊗⊗NATNUM ⊂ ATOM⊗
∂(n)⊗⊗ZERO = {$$0$}⊗
∂(n)⊗⊗NATNUM = ZER0 ∪ POSP⊗
∂(n)⊗⊗ZERO ∩ POSP = qEMPTY⊗
.end

.bb Constants:

.begin nofill turnon"∂" group
.n←20

∂(n)⊗⊗qT ε ATOM⊗
∂(n)⊗⊗qNIL ε NULL⊗
∂(n)⊗⊗qb ε BOTTOM⊗
∂(n)⊗⊗$$0$ ε ZERO⊗
∂(n)⊗⊗$$1,2,...$ ε POSP⊗
.end

.bb Variables:

.begin nofill turnon "∂" group
.n←20

∂(n)⊗⊗X, Y, Z, U, V, W, M, N ε ESEXP⊗
∂(n)⊗⊗x, y, z ε SEXP⊗
∂(n)⊗⊗xx, yy, zz ε PAIR⊗
∂(n)⊗⊗a, b, c ε ATOM⊗
.apart
.group

∂(n)⊗⊗u, v, w ε LIST⊗
∂(n)⊗⊗uu, vv, ww ε NELIST⊗
.apart
.group

∂(n)⊗⊗l, n, m ε NATNUM⊗
∂(n)⊗⊗ll, mm, nn ε POSP⊗
.end

[Remark: If qx is a variable ranging over domain ⊗D then we may also use
qxq0, qxq1, ... as variables ranging over ⊗⊗D⊗].

.bb Function symbols and domain mappings:

The basic function symbols are:
qqa, qqd, qcons, ⊗add1, ⊗sub1, qqat, qqn, qif, qnot, qand, qor.


.begin nofill turnon "∂" group
.n←20

∂(n)⊗⊗qqa: BOTTOM → BOTTOM⊗
∂(n)⊗⊗qqa: PAIR → SEXP⊗
∂(n)⊗⊗qqa: NELIST → SEXP⊗
.apart
.group

∂(n)⊗⊗qqd: BOTTOM → BOTTOM⊗
∂(n)⊗⊗qqd: PAIR → SEXP⊗
∂(n)⊗⊗qqd: NELIST → LIST⊗

∂(n)⊗⊗qcons: BOTTOM qcross ESEXP → BOTTOM⊗
∂(n)⊗⊗qcons: ESEXP qcross BOTTOM → BOTTOM⊗
∂(n)⊗⊗qcons: SEXP qcross SEXP → PAIR⊗
∂(n)⊗⊗qcons: SEXP qcross LIST → NELIST⊗
.apart
.group

∂(n)⊗⊗add1: BOTTOM → BOTTOM⊗
∂(n)⊗⊗add1: NATNUM → POSP⊗
.apart
.group

∂(n)⊗⊗sub1: BOTTOM → BOTTOM⊗
∂(n)⊗⊗sub1: POSP → NATNUM⊗
.end

.bb Algebraic Axioms

.begin nofill turnon "∂" group
.n←20

∂(n)$$CAR:$__⊗⊗∀x y.qa [x_._y] = x⊗
∂(n)$$CDR:$__⊗⊗∀x y.qd [x_._y] = y⊗
∂(n)$$CONS:$__⊗⊗∀xx.[qa xx_._qd xx] = xx⊗
∂(n)$$EQPAIR:$__⊗⊗∀xx yy.[[qa xx = qa yy] ∧ [qd xx = qd yy] ≡ xx = yy]⊗
.apart
.group

∂(n)$$SUB1:$__⊗⊗∀n: sub1 add1 n = n⊗
∂(n)$$ADD1:$__⊗⊗∀nn: add1 sub1 nn = nn⊗
.end

.bb Induction schemata

.begin nofill group

$SEXPINDUCTION: ⊗⊗⊗∀a:qP a ∧ ∀xx:[qP qa xx ∧ qP qd xx ⊃ qP xx] ⊃ ∀x: qP x ⊗.
$LISTINDUCTION: ⊗⊗⊗qP qNIL ∧ ∀uu: [qP qd uu ⊃ qP uu] ⊃ ∀u: qP u ⊗.
$NUMINDUCTION: ⊗⊗⊗qP $0 ∧ ∀nn: [qP sub1 nn ⊃ qP nn] ⊃ ∀n: qP n.⊗
.end

.bb Defining axioms for program primitives

.begin nofill turnon "∂" group
.n←7

$IF: ∂(n)⊗⊗∀X Y Z: qif[X,Y,Z]=IF ¬SEXP X THEN qb ELSE IF X ≠ qNIL THEN Y ELSE Z⊗
     ∂(n)⊗⊗∀x y z: qif[x,y,z] = IF x ≠ qNIL THEN y ELSE z⊗
     ∂(n)⊗⊗qif: SEXP qcross SEXP qcross SEXP → SEXP⊗
.apart
.group

$EQUAL:	∂(n)⊗⊗∀X Y: X equal Y=IF ¬[SEXP X∧SEXP Y] THEN qb ELSE IF X=Y THEN qT ELSE qNIL⊗
        ∂(n)⊗⊗∀x y: [x qequal y] = IF [x = y] THEN qT ELSE qNIL⊗
        ∂(n)⊗⊗qequal: SEXP qcross SEXP → SEXP⊗
.apart
.group

$ATOM:  ∂(n)⊗⊗∀X: qat X=IF ¬SEXP X THEN qb ELSE IF ATOM X THEN qT ELSE qNIL⊗
       	∂(n)⊗⊗∀x: qat x = IF ATOM x THEN qT ELSE qNIL⊗
        ∂(n)⊗⊗qqat: SEXP → SEXP⊗
.apart
.group

$NULL:  ∂(n)⊗⊗∀X: qn X=IF ¬SEXP X THEN qb ELSE IF NULL X THEN qT ELSE qNIL⊗
        ∂(n)⊗⊗∀x: qn x = IF NULL x THEN qT ELSE qNIL⊗
        ∂(n)⊗⊗qqn: SEXP → SEXP⊗
.apart
.group

$NOT:	∂(n)⊗⊗∀X: qnot X = qif[X, qNIL, qT]⊗
      	∂(n)⊗⊗∀x: qnot x = qif x qthen qNIL qelse qT⊗
        ∂(n)⊗⊗qqnot: SEXP → SEXP⊗
.apart
.group

$AND:	∂(n)⊗⊗∀X Y: X qand Y = qif[X,Y,X]⊗
     	∂(n)⊗⊗∀x y: x qand y = qif x qthen y qelse qNIL⊗
        ∂(n)⊗⊗qand: SEXP qcross SEXP → SEXP⊗
.apart
.group

$OR: 	∂(n)⊗⊗∀X Y: X qor Y = qif[X, X, Y]⊗
     	∂(n)⊗⊗∀x y: x or y = qif x qthen x qelse y⊗
        ∂(n)⊗⊗qor: SEXP qcross SEXP → SEXP⊗

.end

.next page
.ss(provinex, Exercises )
.item←0

	The following are properties to prove about programs that
you have written.  The functions and predicates referred to are
described in the Exercises of Chapter {subSECTION WRITINex!}.   You 
should carry out the proofs for your definitions of the indicated functions
or predicates.  You may decide to rewrite your definition because (1) you
find that your function definition is not correct or (2) another definition
is cleaner and more amenable to proofs.  This is quite natural if you are
not thinking in terms of proving it correct when you write the definition.


#. Lists
.begin nofill

	##. ⊗⊗∀u. samelength[u,reverse u]⊗

	##. ⊗⊗∀u v:istail[commontail[u,v],v]⊗
	##. ⊗⊗∀u v:istail[commontail[u,v],u]⊗

	##. ⊗⊗∀u v: commontail[u,v]=commontail[v,u]⊗

	##. ⊗⊗∀u v:[append[upto[commontail[u,v],v],commontail[u,v]]=v]⊗
	##. ⊗⊗∀u v:[append[upto[commontail[u,v],u],commontail[u,v]]=u]⊗

Note that ⊗istail has already been worked on in earlier exercises.  
.end


#. S-expressions

	##. ⊗⊗∀x y:[x ≤ y ⊃ x = get[y,point[x,y]]]⊗

	##. ⊗⊗∀x:[balanced[balance[x]] samefringe[balance[x],x]]⊗

#. Algebra and arithmetic

	##. ⊗⊗∀u v: poly u ∧ poly v ⊃ sum[prod[quot[u,v],v],rem[u,v]⊗

	##. ⊗⊗∀x: arith x ⊃ numval[sop x]]=numval[x]⊗

	Part of the exercise is to invent suitable predicates ⊗poly and ⊗arith
which characterize the domain on which the functions are valid.

#. Sets

	##. ⊗⊗∀x u v:[xε[u∪v] ⊃ xεu ∨ xεv]⊗

	##. ⊗⊗∀x u v:[[xεu] ⊃ ¬xε[v - u]]⊗


#. Permutations

	##. ⊗⊗∀u:[lcycle rcycle u = u]⊗

	##. ⊗⊗∀u:[isperm1 u ⊃ [compose1[p,invert1[p]] = id1⊗

	##. ⊗⊗∀u:[isperm1 u ⊃ [compose1[invert1[p],p] = id1⊗

	##. ⊗⊗u: [isperm1 u ⊃ [invert1 invert1 p = p]]⊗

	##. ⊗⊗∀u v:[isperm2 u ∧ isperm2 v ⊃ rho21[compose2[u,v]] = compose1[rho21 u,rho21 v2]]⊗